proposition: Lemma bin_fun_strext_imp_wd : bin_fun_strext -> bin_fun_wd.
proof: Proof. intros H x1 x2 y1 y2 H0 H1. apply not_ap_imp_eq. intro H2. generalize (H _ _ _ _ H2); intro H3. elim H3; intro H4. now set (eq_imp_not_ap _ _ _ H0). now set (eq_imp_not_ap _ _ _ H1). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid