-lemma apart_symmetric: ∀E.symmetric ? (apart E).
-intros (E); unfold; intros(x y H); cases H; clear H; [right|left] assumption;
+definition apart_of_excedence: excedence → apartness.
+intros (E); apply (mk_apartness E (apart E));
+[1: unfold; cases E; simplify; clear E; intros (x); unfold;
+ intros (H1); apply (H x); cases H1; assumption;
+|2: unfold; intros(x y H); cases H; clear H; [right|left] assumption;
+|3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy);
+ cases Axy (H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
+ [left; left|right; left|right; right|left; right] assumption]