X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fjmeq.ma;h=274ce3d5b32329b4b3cbd07a70a8cf924b79f098;hb=ddc80515997a3f56085c6234d4db326141e189aa;hp=05c13498eff89c5dd4d4bd2559f0c860a49dd072;hpb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;p=helm.git

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index 05c13498e..274ce3d5b 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 in ⊢ (??(???%?)? → ?) #E1
- normalize in E1; >(K ?? E1) normalize
+ generalize {⊢ (??(???%?)? → ?)} #E1
+ normalize {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 in ⊢ (???%); %
+ #A #x #y #E cases E {⊢ (???%)} %
 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 in match E;
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize {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 in H; @(H : PP ? (P b) ?) ]
+  | #H whd {H} @(H : PP ? (P b) ?) ]
 qed.
 
 lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].