proposition: Lemma extension_wd : pred_wd _ P -> (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend.
proof: Proof. intros H H0. red in |- *; intros x y H1 H2. elim H1; intros H3 H4; split. apply H with x; assumption. intro H5; apply H0 with x H3; [ apply H2 | apply H4 ]. Qed.
imports: CoRN.algebra.CSetoids