fact: Record continues_raw (S S': A → Prop) (R R': relation A) := { S_sub: ∀ x, S x → S' x; S_closed: ∀ x y, S' x → S y → R' x y → S x; R_coincides: ∀ x y, S x → S y → (R x y ↔ R' x y) }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)