-
-lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
-intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
-cases (Exy (ap_symmetric ??? a));
-qed.
-
-lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x.
-intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy);
-apply ap_symmetric; assumption;
-qed.