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;
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;