https://github.com/math-comp/analysis/blob/bd05c57283ab3a41dd948e90f26f68c7b8e42cc9/theories/measure_theory/measurable_structure.v#L363 into `sigma_algebraS` ?
analysis/theories/measure_theory/measurable_structure.v
Line 363 in bd05c57
into
sigma_algebraS?