proposition: Lemma fun_strext_imp_wd : fun_strext -> fun_wd.
proof: Proof. intros H x y H0. apply not_ap_imp_eq. intro H1. generalize (H _ _ H1); intro H2. now generalize (eq_imp_not_ap _ _ _ H0). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid