ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
#A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
+(*
ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
+/3/; nqed.
+*)
+
+ntheorem symmetric_not_eq: ∀A:Type. ∀x,y:A. x ≠ y → y ≠ x.
+/3/; nqed.
+
+(*
#A; #x; #y; #H; #K; napply H; napply symmetric_eq; //; nqed.
+*)
ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y.
#A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.