X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=1fdd851e09608171a58ba2a0c5f5f072b5444ba7;hb=ddc80515997a3f56085c6234d4db326141e189aa;hp=bf3bae3a8dc7cb45142b8c2c4657e7953808878c;hpb=409f569bde067546830df25cd0b1ca898573f66a;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index bf3bae3a8..1fdd851e0 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -30,24 +30,29 @@ lemma eq_ind_r :
 
 lemma eq_rect_Type0_r:
   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. 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)
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
   cases p; //; qed.
-  
+
+lemma eq_rect_Type1_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
+  cases p; //; qed.
+
 lemma eq_rect_Type2_r:
   ∀A.∀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)
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
   cases p; //; qed.
 
 lemma eq_rect_Type3_r:
   ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. 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)
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match P})
   cases p; //; qed.
 
 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
 #A #x #P #Hx #y #Heq (cases Heq); //; qed.
 
 theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
-#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed-.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
 
 theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
@@ -56,7 +61,7 @@ theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
 #A #B #Ha #Heq (elim Heq); //; qed.
 
 theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
-#A #x #y #z #H1 #H2 >H1; //; qed-.
+#A #x #y #z #H1 #H2 >H1; //; qed.
 
 theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
 #A #B #f #x #y #H >H; //; qed.