proposition: Lemma W'_common: common W'.
proof: Proof. assert (suspend_restrict: ∀ X x, x ∈ X → suspend (restrict x X) x ≼ X). { intros * inx. split. - intros y [[iny _]| <-]; trivial. - intros y z iny [[inz ltx]|<-] ley. + left; split; trivial. eapply le_lt_trans; eauto. + destruct (classic (x ≼ y)) as [case|case]. * right; apply eqA_spec; auto. * left; split; trivial. apply ltA_spec; auto. } split; unfold W'. - rewrite Wc; apply suspend_restrict; auto. - rewrite Wd, eq_c_d; apply suspend_restrict; auto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)