From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Nov 2011 09:42:37 +0000 (+0000)
Subject: {pattern} => in pattern;
X-Git-Tag: make_still_working~2076
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=94188b0cbaff6340464d90cc13ee246ea7ec3284;p=helm.git

{pattern} => in pattern;
---

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b059991..b616a824b 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -128,7 +128,7 @@ EXTEND
   ];
   pattern_spec: [
     [ res = OPT [
-       SYMBOL "{";
+       "in" ;
        wanted_and_sps =
         [ "match" ; wanted = tactic_term ;
           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
@@ -136,7 +136,7 @@ EXTEND
         | sps = sequent_pattern_spec ->
            None,Some sps
         ];
-       SYMBOL "}" ->
+       SYMBOL ";" ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
              wanted,None -> wanted, [], Some N.UserInput
diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml
index 8cd75e228..dbb6900d9 100644
--- a/matita/matita/help/C/sec_terms.xml
+++ b/matita/matita/help/C/sec_terms.xml
@@ -636,18 +636,18 @@
        <row>
 	<entry id="grammar.pattern">&pattern;</entry>
 	<entry>::=</entry>
-        <entry><emphasis role="bold">{</emphasis>
+        <entry><emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>simple pattern</entry>
        </row>
        <row>
         <entry/>
         <entry>|</entry>
-        <entry><emphasis role="bold">{match</emphasis> &path;
+        <entry><emphasis role="bold">in</emphasis> <emphasis role="bold">match</emphasis> &path;
           [<emphasis role="bold">in</emphasis>
           [&id;[<emphasis role="bold">:</emphasis> &path;]]…
-          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">}</emphasis></entry>
+          [<emphasis role="bold">⊢</emphasis> &path;]]<emphasis role="bold">;</emphasis></entry>
         <entry>full pattern</entry>
        </row>
       </tbody>
@@ -655,7 +655,7 @@
     </table>
     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
       <title>path</title>
-      <tgroup cols="4">
+      <tgroup cols="3">
       <tbody>
        <row>
 	<entry id="grammar.path">&path;</entry>
diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml
index c7a789c1a..12e450fdf 100644
--- a/matita/matita/help/C/tactics_quickref.xml
+++ b/matita/matita/help/C/tactics_quickref.xml
@@ -5,175 +5,115 @@
       <row>
         <entry id="grammar.tactic">&tactic;</entry>
         <entry>::=</entry>
-        <entry><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
         <entry>
-          <link linkend="tac_assumption">
-            <emphasis role="bold">assumption</emphasis>
+          <link linkend="tac_#">
+            <emphasis role="bold">#</emphasis>
           </link>
+          <emphasis>
+            <link linkend="grammar.id">id</link>
+          </emphasis>
         </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis>. <emphasis role="bold">autobatch</emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-	     <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
-	     <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
-	    </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-	     <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
-	     <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
-	    </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_compose"><emphasis role="bold">compose</emphasis></link> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] [<emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>]</entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></entry>
+          <link linkend="tac_##">
+            <emphasis role="bold">##</emphasis>
+          </link>
+        </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_contradiction">
-            <emphasis role="bold">contradiction</emphasis>
+          <link linkend="tac_#_">
+            <emphasis role="bold">#_</emphasis>
           </link>
         </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+        <entry><link linkend="tac_%"><emphasis role="bold">%</emphasis></link> [<emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bol">{</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…<emphasis role="bol">}</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-	     <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
-	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
+	     <link linkend="tac_*"><emphasis role="bold">*</emphasis></link>
+	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_demodulate"><emphasis role="bold">demodulate</emphasis></link> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry>
+	     <link linkend="tac_-"><emphasis role="bold">-</emphasis></link><emphasis><link linkend="grammar.id">id</link></emphasis>
+	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+        <entry><emphasis role="bold">/</emphasis><emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis><emphasis role="bold">/</emphasis>. </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+        <entry>[<emphasis role="bold">&lt;</emphasis>|<link linkend="tac_&gt;"><emphasis role="bold">&gt;</emphasis></link>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+        <entry><link linkend="tac_@"><emphasis role="bold">@</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>
-          <link linkend="tac_exists">
-            <emphasis role="bold">exists</emphasis>
-          </link>
-        </entry>
+        <entry><link linkend="tac_applyS"><emphasis role="bold">applyS</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.autoparams">auto_params</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_fail">
-            <emphasis role="bold">fail</emphasis>
+          <link linkend="tac_assumption">
+            <emphasis role="bold">assumption</emphasis>
           </link>
         </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
         <entry>
-          <link linkend="tac_fourier">
-            <emphasis role="bold">fourier</emphasis>
-          </link>
-        </entry>
+	     <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
+	     <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
+	    </entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</entry>
+        <entry><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+        <entry><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry>
-          <link linkend="tac_id">
-            <emphasis role="bold">id</emphasis>
-          </link>
-        </entry>
+        <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link>
+             [<emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>] [<emphasis role="bold">skip</emphasis> <emphasis role="bold">(</emphasis><emphasis><link linkend="grammar.id">id</link></emphasis>…<emphasis role="bold">)</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</entry>
+        <entry><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></entry>
+        <entry><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
       </row>
       <row>
         <entry/>
@@ -185,25 +125,9 @@
         <entry>|</entry>
         <entry>
 	     <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> 
-	     [<emphasis role="bold">linear</emphasis>]
-	     [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] 
 	     <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> 
-	     [<emphasis role="bold">to</emphasis>
-	      <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
-	      [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
-	     ] 
-	     [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
 	    </entry>
       </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_left">
-            <emphasis role="bold">left</emphasis>
-          </link>
-        </entry>
-      </row>
       <row>
         <entry/>
         <entry>|</entry>
@@ -212,91 +136,13 @@
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_reflexivity">
-            <emphasis role="bold">reflexivity</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_right">
-            <emphasis role="bold">right</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_ring">
-            <emphasis role="bold">ring</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_split">
-            <emphasis role="bold">split</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_subst">
-            <emphasis role="bold">subst</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry>
-          <link linkend="tac_symmetry">
-            <emphasis role="bold">symmetry</emphasis>
-          </link>
-        </entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
-      </row>
-      <row>
-        <entry/>
-        <entry>|</entry>
-        <entry><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis>
+             [<emphasis role="bold">nodelta</emphasis>]</entry>
       </row>
       <row>
         <entry/>
         <entry>|</entry>
-        <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></entry>
+        <entry><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">nodelta</emphasis>]</entry>
       </row>
     </tbody>
   </tgroup>
diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index 274ce3d5b..42e52c0a4 100644
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -57,14 +57,14 @@ qed.
 lemma gral: ∀A.∀x,y:A.
  mk_Sigma A x = mk_Sigma A y → x=y.
  #A #x #y #E lapply (tech1 ?? E)
- generalize {⊢ (??(???%?)? → ?)} #E1
- normalize {E1}; >(K ?? E1) normalize
+ generalize in ⊢ (??(???%?)? → ?); #E1
+ normalize in E1; >(K ?? E1) normalize
  #H @H
 qed.
 
 lemma jm_to_eq_sigma:
  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
- #A #x #y #E cases E {⊢ (???%)} %
+ #A #x #y #E cases E in ⊢ (???%); %
 qed.
 
 definition curry:
@@ -77,7 +77,7 @@ qed.
 lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
  P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
   P y h.
- #A #x #P #H #y #E lapply (gral ??? E) #G generalize {match E}
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
  @(match G
     return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
    with
@@ -94,7 +94,7 @@ lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
  #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
  lapply (G ?? (curry ?? P) ?? F)
   [ normalize //
-  | #H whd {H} @(H : PP ? (P b) ?) ]
+  | #H whd in H; @(H : PP ? (P b) ?) ]
 qed.
 
 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 1fdd851e0..c80fa31f5 100644
--- 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.