From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 25 Jul 2005 17:59:34 +0000 (+0000)
Subject: Notation for equality used everywhere.
X-Git-Tag: V_0_7_2~76
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=633474751ddf1074947ff0d324fb1aca2293eff8;p=helm.git

Notation for equality used everywhere.

Note: due to a bug in the notation machinery, the declaration of the notation
is a bit cumbersome (it uses a URI and an alias; it should use no alias and
just eq in place of the URI). To be fixed.
---

diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index bdea562ce..e8fbb6dd9 100644
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -19,18 +19,18 @@ include "logic/connectives.ma".
 
 definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
-  \forall x,y:A.eq B (f x) (f y) \to (eq A x y).
+  \forall x,y:A.f x = f y \to x=y.
 
 (* we have still to attach exists *)
 definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
-  \forall z:B.ex A (\lambda x:A.(eq B z (f x))).
+  \forall z:B.ex A (\lambda x:A.z=f x).
 
 definition symmetric: \forall A:Type.\forall f:A \to A\to A.Prop
-\def \lambda A.\lambda f.\forall x,y.eq A (f x y) (f y x).
+\def \lambda A.\lambda f.\forall x,y.f x y = f y x.
 
 definition associative: \forall A:Type.\forall f:A \to A\to A.Prop
-\def \lambda A.\lambda f.\forall x,y,z.eq A (f (f x y) z) (f x (f y z)).
+\def \lambda A.\lambda f.\forall x,y,z.f (f x y) z = f x (f y z).
 
 (* functions and relations *)
 definition monotonic : \forall A:Type.\forall R:A \to A \to Prop.
@@ -39,6 +39,6 @@ definition monotonic : \forall A:Type.\forall R:A \to A \to Prop.
 
 (* functions and functions *)
 definition distributive: \forall A:Type.\forall f,g:A \to A \to A.Prop
-\def \lambda A.\lambda f,g.\forall x,y,z:A.eq A (f x (g y z)) (g (f x y) (f x z)).
+\def \lambda A.\lambda f,g.\forall x,y,z:A. f x (g y z) = g (f x y) (f x z).
 
 
diff --git a/helm/matita/library/higher_order_defs/ordering.ma b/helm/matita/library/higher_order_defs/ordering.ma
index a945805da..c2b351d7a 100644
--- a/helm/matita/library/higher_order_defs/ordering.ma
+++ b/helm/matita/library/higher_order_defs/ordering.ma
@@ -18,5 +18,5 @@ include "logic/equality.ma".
 
 definition antisymmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop
 \def 
-\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to (eq A x y).
+\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to x=y.
 
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index fb7e66edf..0be69f9b7 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -18,6 +18,11 @@ include "higher_order_defs/relations.ma".
 
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.
+
+interpretation "leibnitz's equality"
+   'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
     
 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
 simplify.intros.apply refl_eq.
@@ -27,19 +32,19 @@ theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
 simplify.intros.elim H. apply refl_eq.
 qed.
 
-theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y  \to eq A y x
+theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
 simplify.intros.elim H1.assumption.
 qed.
 
-theorem trans_eq : \forall A:Type.\forall x,y,z:A. eq A x y  \to eq A y z \to eq A x z
+theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
 \def transitive_eq.
 
 theorem eq_elim_r:
  \forall A:Type.\forall x:A. \forall P: A \to Prop.
-   P x \to \forall y:A. eq A y x \to P y.
+   P x \to \forall y:A. y=x \to P y.
 intros. elim sym_eq ? ? ? H1.assumption.
 qed.
 
@@ -51,12 +56,12 @@ default "equality"
  cic:/matita/logic/equality/eq_elim_r.con. 
  
 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
-\forall x,y:A. eq A x y \to eq B (f x) (f y).
+\forall x,y:A. x=y \to (f x)=(f y).
 intros.elim H.reflexivity.
 qed.
 
 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 \forall x1,x2:A. \forall y1,y2:B.
-eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
+x1=x2 \to y1=y2 \to (f x1 y1)=(f x2 y2).
 intros.elim H1.elim H.reflexivity.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index fec46ae2f..16d689e4c 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -67,26 +67,26 @@ match n with
       [ O \Rightarrow GT
       | (S q) \Rightarrow nat_compare p q]].
 
-theorem nat_compare_n_n: \forall n:nat.(eq compare (nat_compare n n) EQ).
+theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
 intro.elim n.
 simplify.reflexivity.
 simplify.assumption.
 qed.
 
 theorem nat_compare_S_S: \forall n,m:nat. 
-eq compare (nat_compare n m) (nat_compare (S n) (S m)).
+nat_compare n m = nat_compare (S n) (S m).
 intros.simplify.reflexivity.
 qed.
 
 theorem nat_compare_to_Prop: \forall n,m:nat. 
 match (nat_compare n m) with
   [ LT \Rightarrow (lt n m)
-  | EQ \Rightarrow (eq nat n m)
+  | EQ \Rightarrow n=m
   | GT \Rightarrow (lt m n) ].
 intros.
 apply nat_elim2 (\lambda n,m.match (nat_compare n m) with
   [ LT \Rightarrow (lt n m)
-  | EQ \Rightarrow (eq nat n m)
+  | EQ \Rightarrow n=m
   | GT \Rightarrow (lt m n) ]).
 intro.elim n1.simplify.reflexivity.
 simplify.apply le_S_S.apply le_O_n.
@@ -98,9 +98,9 @@ simplify. apply eq_f. apply H.
 qed.
 
 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
-eq compare (nat_compare n m) (compare_invert (nat_compare m n)).
+nat_compare n m = compare_invert (nat_compare m n).
 intros. 
-apply nat_elim2 (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))).
+apply nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)).
 intros.elim n1.simplify.reflexivity.
 simplify.reflexivity.
 intro.elim n1.simplify.reflexivity.
@@ -109,12 +109,12 @@ intros.simplify.elim H.reflexivity.
 qed.
      
 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
-((lt n m) \to (P LT)) \to ((eq nat n m) \to (P EQ)) \to ((lt m n) \to (P GT)) \to 
+((lt n m) \to (P LT)) \to (n=m \to (P EQ)) \to ((lt m n) \to (P GT)) \to 
 (P (nat_compare n m)).
 intros.
 cut match (nat_compare n m) with
 [ LT \Rightarrow (lt n m)
-| EQ \Rightarrow (eq nat n m)
+| EQ \Rightarrow n=m
 | GT \Rightarrow (lt m n)] \to
 (P (nat_compare n m)).
 apply Hcut.apply nat_compare_to_Prop.
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 2b00a97ab..4c43d33bd 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -71,7 +71,7 @@ apply le_n.
 qed.
 
 theorem div_aux_mod_aux: \forall p,n,m:nat. 
-(eq nat n (plus (times (div_aux p n m) (S m)) (mod_aux p n m) )).
+(n=plus (times (div_aux p n m) (S m)) (mod_aux p n m)).
 intro.elim p.
 simplify.elim leb n m.
 simplify.apply refl_eq.
@@ -82,7 +82,7 @@ simplify.intro.apply refl_eq.
 simplify.intro.
 rewrite > assoc_plus. 
 elim (H (minus n1 (S m)) m).
-change with (eq nat n1 (plus (S m) (minus n1 (S m)))).
+change with (n1=plus (S m) (minus n1 (S m))).
 rewrite < sym_plus.
 apply plus_minus_m_m.
 change with lt m n1.
@@ -90,7 +90,7 @@ apply not_le_to_lt.exact H1.
 qed.
 
 theorem div_mod: \forall n,m:nat. 
-(lt O m) \to (eq nat n (plus (times (div n m) m) (mod n m))).
+(lt O m) \to n=plus (times (div n m) m) (mod n m).
 intros 2.elim m.elim (not_le_Sn_O O H).
 simplify.
 apply div_aux_mod_aux.
@@ -98,14 +98,14 @@ qed.
 
 inductive div_mod_spec (n,m,q,r:nat) : Prop \def
 div_mod_spec_intro: 
-(lt r m) \to (eq nat n (plus (times q m) r)) \to (div_mod_spec n m q r).
+(lt r m) \to n=plus (times q m) r \to (div_mod_spec n m q r).
 
 (* 
 definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
-\lambda n,m,q,r:nat.(And (lt r m) (eq nat n (plus (times q m) r))).
+\lambda n,m,q,r:nat.(And (lt r m) n=plus (times q m) r).
 *)
 
-theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to Not (eq nat m O).
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to Not (m=O).
 intros 4.simplify.intros.elim H.absurd le (S r) O.
 rewrite < H1.assumption.
 exact not_le_Sn_O r.
@@ -175,4 +175,4 @@ apply H5.
 apply le_times_r.
 apply lt_to_le.
 apply H6.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index b6e7fc5e2..b4cff5d58 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -27,28 +27,28 @@ let rec minus n m \def
         | (S q) \Rightarrow minus p q ]].
 
 
-theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
+theorem minus_n_O: \forall n:nat.n=minus n O.
 intros.elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
+theorem minus_n_n: \forall n:nat.O=minus n n.
 intros.elim n.simplify.
 reflexivity.
 simplify.apply H.
 qed.
 
-theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
+theorem minus_Sn_n: \forall n:nat. S O = minus (S n) n.
 intro.elim n.
 simplify.reflexivity.
 elim H.reflexivity.
 qed.
 
 theorem minus_Sn_m: \forall n,m:nat. 
-le m n \to eq nat (minus (S n) m) (S (minus n m)).
+le m n \to minus (S n) m = S (minus n m).
 intros 2.
 apply nat_elim2
-(\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
+(\lambda n,m.le m n \to minus (S n) m = S (minus n m)).
 intros.apply le_n_O_elim n1 H.
 simplify.reflexivity.
 intros.simplify.reflexivity.
@@ -57,10 +57,10 @@ apply le_S_S_to_le. assumption.
 qed.
 
 theorem plus_minus:
-\forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
+\forall n,m,p:nat. le m n \to plus (minus n m) p = minus (plus n p) m.
 intros 2.
 apply nat_elim2
-(\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
+(\lambda n,m.\forall p:nat.le m n \to plus (minus n m) p = minus (plus n p) m).
 intros.apply le_n_O_elim ? H.
 simplify.rewrite < minus_n_O.reflexivity.
 intros.simplify.reflexivity.
@@ -68,9 +68,9 @@ intros.simplify.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem plus_minus_m_m: \forall n,m:nat.
-le m n \to eq nat n (plus (minus n m) m).
+le m n \to n = plus (minus n m) m.
 intros 2.
-apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
+apply nat_elim2 (\lambda n,m.le m n \to n = plus (minus n m) m).
 intros.apply le_n_O_elim n1 H.
 reflexivity.
 intros.simplify.rewrite < plus_n_O.reflexivity.
@@ -79,8 +79,8 @@ apply eq_f.rewrite < sym_plus.apply H.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to 
-eq nat n (plus m p).
+theorem minus_to_plus :\forall n,m,p:nat.le m n \to minus n m = p \to 
+n = plus m p.
 intros.apply trans_eq ? ? (plus (minus n m) m) ?.
 apply plus_minus_m_m.
 apply H.elim H1.
@@ -88,7 +88,7 @@ apply sym_plus.
 qed.
 
 theorem plus_to_minus :\forall n,m,p:nat.le m n \to
-eq nat n (plus m p) \to eq nat (minus n m) p.
+n = plus m p \to minus n m = p.
 intros.
 apply inj_plus_r m.
 rewrite < H1.
@@ -98,9 +98,9 @@ apply plus_minus_m_m.assumption.
 qed.
 
 theorem eq_minus_n_m_O: \forall n,m:nat.
-le n m \to eq nat (minus n m) O.
+le n m \to minus n m = O.
 intros 2.
-apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
+apply nat_elim2 (\lambda n,m.le n m \to minus n m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
 (* ancora problemi con il not *)
@@ -130,8 +130,8 @@ theorem distributive_times_minus: distributive nat times minus.
 simplify.
 intros.
 apply (leb_elim z y).intro.
-cut eq nat (plus (times x (minus y z)) (times x z)) 
-           (plus (minus (times x y) (times x z)) (times x z)).
+cut plus (times x (minus y z)) (times x z) =
+    plus (minus (times x y) (times x z)) (times x z).
 apply inj_plus_l (times x z).
 assumption.
 apply trans_eq nat ? (times x y).
@@ -151,7 +151,7 @@ apply not_le_to_lt.assumption.
 qed.
 
 theorem distr_times_minus: \forall n,m,p:nat.
-eq nat (times n (minus m p)) (minus (times n m) (times n p))
+times n (minus m p) = minus (times n m) (times n p)
 \def distributive_times_minus.
 
 theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index f84ffef44..100a101f9 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -27,8 +27,7 @@ definition pred: nat \to nat \def
 [ O \Rightarrow  O
 | (S p) \Rightarrow p ].
 
-theorem pred_Sn : \forall n:nat.
-(eq nat n (pred (S n))).
+theorem pred_Sn : \forall n:nat.n=(pred (S n)).
 intros; reflexivity.
 qed.
 
@@ -40,12 +39,11 @@ rewrite > pred_Sn y.
 apply eq_f. assumption.
 qed.
 
-theorem inj_S : \forall n,m:nat. 
-(eq nat (S n) (S m)) \to (eq nat n m)
+theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 \def injective_S.
 
 theorem not_eq_S  : \forall n,m:nat. 
-Not (eq nat n m) \to Not (eq nat (S n) (S m)).
+Not (n=m) \to Not (S n = S m).
 intros. simplify. intros.
 apply H. apply injective_S. assumption.
 qed.
@@ -56,14 +54,14 @@ definition not_zero : nat \to Prop \def
   [ O \Rightarrow False
   | (S p) \Rightarrow True ].
 
-theorem not_eq_O_S : \forall n:nat. Not (eq nat O (S n)).
+theorem not_eq_O_S : \forall n:nat. Not (O=S n).
 intros. simplify. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 qed.
 
-theorem not_eq_n_Sn : \forall n:nat. Not (eq nat n (S n)).
+theorem not_eq_n_Sn : \forall n:nat. Not (n=S n).
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 34cd6f6a3..3f788c650 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -84,7 +84,7 @@ apply le_S_S_to_le.assumption.
 qed.
 
 (* ??? this needs not le *)
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+theorem S_pred: \forall n:nat.lt O n \to n=S (pred n).
 intro.elim n.apply False_ind.exact not_le_Sn_O O H.
 apply eq_f.apply pred_Sn.
 qed.
@@ -112,7 +112,7 @@ apply H2.apply lt_to_le. apply H3.
 qed.
 
 (* le elimination *)
-theorem le_n_O_to_eq : \forall n:nat. (le n O) \to (eq nat O n).
+theorem le_n_O_to_eq : \forall n:nat. (le n O) \to O=n.
 intro.elim n.reflexivity.
 apply False_ind.
 (* non si applica not_le_Sn_O *)
@@ -128,7 +128,7 @@ apply  (not_le_Sn_O ? H1).
 qed.
 
 theorem le_n_Sm_elim : \forall n,m:nat.le n (S m) \to 
-\forall P:Prop. (le (S n) (S m) \to P) \to (eq nat n (S m) \to P) \to P.
+\forall P:Prop. (le (S n) (S m) \to P) \to (n=(S m) \to P) \to P.
 intros 4.elim H.
 apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
@@ -137,7 +137,7 @@ qed.
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
 simplify.intros 2.
-apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)).
+apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to n=m)).
 intros.apply le_n_O_to_eq.assumption.
 intros.apply False_ind.apply not_le_Sn_O ? H.
 intros.apply eq_f.apply H.
@@ -145,7 +145,7 @@ apply le_S_S_to_le.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
-theorem antisym_le: \forall n,m:nat. le n m \to le m n \to eq nat n m
+theorem antisym_le: \forall n,m:nat. le n m \to le m n \to n=m
 \def antisymmetric_le.
 
 theorem decidable_le: \forall n,m:nat. decidable (le n m).
@@ -156,4 +156,4 @@ intros.simplify.right.exact not_le_Sn_O n1.
 intros 2.simplify.intro.elim H.
 left.apply le_S_S.assumption.
 right.intro.apply H1.apply le_S_S_to_le.assumption.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma
index 32a58115d..fbfad715c 100644
--- a/helm/matita/library/nat/orders_op.ma
+++ b/helm/matita/library/nat/orders_op.ma
@@ -52,7 +52,7 @@ intros.change with le (plus O m) (plus n m).
 apply le_plus_l.apply le_O_n.
 qed.
 
-theorem eq_plus_to_le: \forall n,m,p:nat.eq nat n (plus m p) 
+theorem eq_plus_to_le: \forall n,m,p:nat.n=plus m p
 \to le m n.
 intros.rewrite > H.
 rewrite < sym_plus.
diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index e8750d0cb..39e48f21e 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -21,13 +21,13 @@ let rec plus n m \def
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ].
 
-theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
+theorem plus_n_O: \forall n:nat. n = plus n O.
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).
+theorem plus_n_Sm : \forall n,m:nat. S (plus n  m) = plus n (S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
@@ -38,7 +38,7 @@ and functions/symmetric; functions symmetric is not in
 functions.moo why?
 theorem symmetric_plus: symmetric nat plus. *)
 
-theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n).
+theorem sym_plus: \forall n,m:nat. plus n m = plus m n.
 intros.elim n.
 simplify.apply plus_n_O.
 simplify.rewrite > H.apply plus_n_Sm.
@@ -50,7 +50,7 @@ simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
 
-theorem assoc_plus : \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p))
+theorem assoc_plus : \forall n,m,p:nat. plus (plus n m) p = plus n (plus m p)
 \def associative_plus.
 
 theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.plus n m).
@@ -59,7 +59,7 @@ exact H.
 apply H.apply inj_S.apply H1.
 qed.
 
-theorem inj_plus_r: \forall p,n,m:nat.eq nat (plus p n) (plus p m) \to (eq nat n m)
+theorem inj_plus_r: \forall p,n,m:nat. plus p n = plus p m \to n=m
 \def injective_plus_r.
 
 theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.plus n m).
@@ -71,5 +71,5 @@ rewrite < sym_plus y.
 assumption.
 qed.
 
-theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m)
+theorem inj_plus_l: \forall p,n,m:nat. plus n p = plus m p \to n=m
 \def injective_plus_l.
diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 953b3a1b6..035116d0f 100644
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -23,14 +23,14 @@ let rec times n m \def
  [ O \Rightarrow O
  | (S p) \Rightarrow (plus m (times p m)) ].
 
-theorem times_n_O: \forall n:nat. eq nat O (times n O).
+theorem times_n_O: \forall n:nat. O = times n O.
 intros.elim n.
 simplify.reflexivity.
 simplify.assumption.
 qed.
 
 theorem times_n_Sm : 
-\forall n,m:nat. eq nat (plus n (times n  m)) (times n (S m)).
+\forall n,m:nat.plus n (times n  m) = times n (S m).
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.rewrite < H.
@@ -46,7 +46,7 @@ qed.
 theorem symmetric_times : symmetric nat times. *)
 
 theorem sym_times : 
-\forall n,m:nat. eq nat (times n m) (times m n).
+\forall n,m:nat.times n m = times m n.
 intros.elim n.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
@@ -62,6 +62,6 @@ rewrite > assoc_plus.reflexivity.
 qed.
 
 variant times_plus_distr: \forall n,m,p:nat.
-eq nat (times n (plus m p)) (plus (times n m) (times n p))
+times n (plus m p) = plus (times n m) (times n p)
 \def distributive_times_plus.