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