X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fjmeq.ma;h=42e52c0a430a40ee20a133a2f23c283bff7b00e2;hb=94188b0cbaff6340464d90cc13ee246ea7ec3284;hp=274ce3d5b32329b4b3cbd07a70a8cf924b79f098;hpb=e28ee799d0281fb76d484d9b4c01d8bed4716bbe;p=helm.git

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].