https://github.com/math-comp/analysis/blob/7c12c63fbd3238e1004351bd393b3d33e6a21258/theories/measure.v#L869 `G` does not need to be `dynkin`...
analysis/theories/measure.v
Line 869 in 7c12c63
Gdoes not need to bedynkin...