{pattern} => in pattern;

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b059991db9e8b21093f531b2413ff4c802841a..b616a824b2d8c547a80cce9ae440ed9b114be7e3 100644 (file)
--- 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 8cd75e22808abc945e998ee568fe1aeb515dcba7..dbb6900d98f9d92d17184070315b0e7adf6d42f9 100644 (file)
--- 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 c7a789c1a32ed246648eb8577e80afb34aa77862..12e450fdf49da7e988b91a4790a25f50eb9e7043 100644 (file)
--- 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 274ce3d5b32329b4b3cbd07a70a8cf924b79f098..42e52c0a430a40ee20a133a2f23c283bff7b00e2 100644 (file)
--- 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 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.