proposition: Lemma bpfwdef : forall S1 S2 (F : BinPartFunct S1 S2) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy.
proof: Proof. intros. apply not_ap_imp_eq; intro H0. generalize (bpfstrx _ _ _ _ _ _ _ H0). exact (eq_imp_not_ap _ _ _ H). Qed.
imports: CoRN.algebra.CSetoids