X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2FPlogic%2Fequality.ma;h=4195c06f66ab04498a6e9fd6c0ea30cca0c4518e;hb=HEAD;hp=a5972e2709446cce6a401ba28c228e93920b54ac;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/nlibrary/Plogic/equality.ma b/matita/matita/nlibrary/Plogic/equality.ma
index a5972e270..4195c06f6 100644
--- a/matita/matita/nlibrary/Plogic/equality.ma
+++ b/matita/matita/nlibrary/Plogic/equality.ma
@@ -14,57 +14,57 @@
 
 include "logic/pts.ma".
 
-ninductive eq (A:Type[2]) (x:A) : A → Prop ≝
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
     refl: eq A x x.
     
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
-nlemma eq_rect_r:
- ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; #P; #H; nassumption.
-nqed.
+lemma eq_rect_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
+ #A  #a  #x  #p  cases p  #P  #H  assumption.
+qed.
 
-nlemma eq_ind_r :
+lemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
-nqed.
+ #A #a #P #p #x0 #p0 apply (eq_rect_r ? ? ? p0) assumption.
+qed.
 
-nlemma eq_rect_Type2_r :
-  ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
-  #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P;
-  ncases p;//;
-nqed.
+lemma eq_rect_Type2_r :
+  ∀A:Type[0].∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p generalize in match H generalize in match P 
+  cases p // 
+qed.
 
 (*
 nlemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; ngeneralize in match p; 
-ncases p0; #Heq; nassumption.
+ #A  #a  #P  #p  #x0  #p0  ngeneralize in match p  
+ncases p0  #Heq  nassumption.
 nqed.
 *)
 
-ntheorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
-#A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
-nqed. 
+theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
+#A  #x  #P  #Hx  #y  #Heq cases Heq assumption.
+qed. 
 
-ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
-#A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x)); 
-##[ @; ##| nassumption; ##]
-nqed.
+theorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
+#A  #x  #y  #Heq  apply (rewrite_l A x (λz.z=x))  
+[ % | assumption ]
+qed.
 
-ntheorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
-#A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
-nqed.
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
+#A  #x  #P  #Hx  #y  #Heq  cases (sym_eq ? ? ?Heq)  assumption.
+qed.
 
-ntheorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
-#A; #B; #Ha; #Heq;nelim Heq; nassumption.
-nqed.
+theorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
+#A  #B  #Ha  #Heq elim Heq  assumption.
+qed.
 
-ndefinition R0 ≝ λT:Type[0].λt:T.t.
+definition R0 ≝ λT:Type[0].λt:T.t.
   
-ndefinition R1 ≝ eq_rect_Type0.
+definition R1 ≝ eq_rect_Type0.
 
-ndefinition R2 :
+definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
@@ -76,13 +76,13 @@ ndefinition R2 :
   ∀b1: T1 b0 e0.
   ∀e1:R1 ?? T1 a1 ? e0 = b1.
   T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
-napply (eq_rect_Type0 ????? e1);
-napply (R1 ?? ? ?? e0);
-napply a2;
-nqed.
+#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 
+apply (eq_rect_Type0 ????? e1) 
+apply (R1 ?? ? ?? e0) 
+apply a2 
+qed.
 
-ndefinition R3 :
+definition R3 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
@@ -99,13 +99,13 @@ ndefinition R3 :
   ∀b2: T2 b0 e0 b1 e1.
   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
   T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
-napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ???? e0 ? e1);
-napply a3;
-nqed.
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 
+apply (eq_rect_Type0 ????? e2) 
+apply (R2 ?? ? ???? e0 ? e1) 
+apply a3 
+qed.
 
-ndefinition R4 :
+definition R4 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
@@ -134,10 +134,10 @@ ndefinition R4 :
   ∀b3: T3 b0 e0 b1 e1 b2 e2.
   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
   T4 b0 e0 b1 e1 b2 e2 b3 e3.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
-napply (eq_rect_Type0 ????? e3);
-napply (R3 ????????? e0 ? e1 ? e2);
-napply a4;
-nqed.
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3 
+apply (eq_rect_Type0 ????? e3) 
+apply (R3 ????????? e0 ? e1 ? e2) 
+apply a4 
+qed.
 
-naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
\ No newline at end of file
+axiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.