proposition: Lemma union_ub B (bound: ∀ S, F S → S ≼ B): union ≼ B.
proof: Proof. split. - intros x [S [inS inx]]; apply (bound S inS), inx. - intros ?? inx [S [inS inY]] lexy. exists S; split; trivial. eapply cs_closed; eauto. apply bound, inS. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)