fact: Record closed_subset s₁ s₂ := { cs_subset: s₁ ⊆ s₂; cs_closed: ∀ x y, x ∈ s₂ → y ∈ s₁ → x ≼ y → x ∈ s₁ }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)