{pattern} => in pattern;

[helm.git] / matita / matita / lib / basics / logic.ma

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 1fdd851e09608171a58ba2a0c5f5f072b5444ba7..c80fa31f55c5469a97212e3c49431360e3e805fa 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -30,22 +30,22 @@ 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 {match H}) (generalize {match P})
+  #A #a #P #H #x #p lapply H lapply 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})
+  #A #a #P #H #x #p lapply H lapply 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 {match H}) (generalize {match P})
+  #A #a #P #H #x #p lapply H lapply 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 {match H}) (generalize {match P})
+  #A #a #P #H #x #p lapply H lapply P
   cases p; //; qed.
 
 theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.