proposition: Corollary W'_le_W: W' ≼ W.
proof: Proof. apply prefix_union; auto using common_comparable, W'_common. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)