proposition: Lemma W_gset: gset W.
proof: Proof. split; auto using W_wo. intros b inb. rewrite Wc. enough (restrict b (restrict c C) ≌ restrict b C) as ->. { apply C_bounds; auto. destruct inb as [X [[[subX _] _] inb]]. apply subX in inb; trivial. } apply subset_equ. - clear; firstorder. - intro x; intros [inx ltb]; repeat (split; trivial). rewrite ltb. apply upper_bound with W; auto using W_wo. rewrite Wc. apply C_bounds; auto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)