proposition: Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP.
proof: Proof. intros H H0. red in |- *; intros x y H1 H2. inversion_clear H1; split. apply H with x; assumption. apply H0 with x; assumption. Qed.
imports: CoRN.algebra.CSetoids