X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fjmeq.ma;h=42e52c0a430a40ee20a133a2f23c283bff7b00e2;hb=ea368a02a071bb99eeb84bf24ab4000acb314d60;hp=05c13498eff89c5dd4d4bd2559f0c860a49dd072;hpb=2343da541bb828ac61079d7811c0fe5613b04fb6;p=helm.git

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index 05c13498e..42e52c0a4 100644
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -57,7 +57,7 @@ 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
+ generalize in ⊢ (??(???%?)? → ?); #E1
  normalize in E1; >(K ?? E1) normalize
  #H @H
 qed.