-[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 H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1;
- [left; left|right; left|right; right|left; right] assumption]
+[1: intro x; simplify; intro H; cases H; clear H;
+ apply (exc_coreflexive x H1);
+|2: intros 3 (x y H); simplify in H ⊢ %; cases H; [right|left]assumption;
+|3: intros 4 (x y z H); simplify in H ⊢ %; cases H; clear H;
+ [ cases (exc_cotransitive x y z H1); [left;left|right;left] assumption;
+ | cases (exc_cotransitive y x z H1); [right;right|left;right] assumption;]]