proposition: Lemma prefix_union S (inS: F S): S ≼ union.
proof: Proof. split. - exists S; auto. - intros ?? [S' [inS' inx]] iny lexy. destruct (chain S S') as [[sub cl]|[sub cl]]; eauto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)