// in place of nauto everywhere

[helm.git] / helm / software / matita / nlibrary / basics / eq.ma

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
index 6ccfa625963a38f0e601b738f170c4138794a510..73abc9f09c2098b14ff5982f7deef0aedda47ccd 100644 (file)
--- a/helm/software/matita/nlibrary/basics/eq.ma
+++ b/helm/software/matita/nlibrary/basics/eq.ma
@@ -23,13 +23,13 @@ ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
 //; nqed.
 
 ntheorem transitive_eq : ∀A:Type. transitive A (eq A).
-//; nqed.
+#A; #x; #y; #z; #H1; #H2; nrewrite > H1; //; nqed.
 
 ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y).
-/2/; 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.
-//; nqed.
+#A; #B; #f; #x; #y; #H; nrewrite > H; //; nqed.
 
 (*
 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
@@ -39,4 +39,5 @@ qed. *)
 
 ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
-//; nqed.
\ No newline at end of file
+#A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
+nqed.
\ No newline at end of file