proposition: Corollary W'_gset: gset W'.
proof: Proof. apply suspend_bound_gset; auto using W_gset. rewrite Wc; apply C_bounds; trivial. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)