fact: Record gset C := { C_wo:> well_ordered C; C_bounds: ∀ c, c ∈ C → g (restrict c C) c }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)