A few integrations (closed an axiom in finset).

[helm.git] / matita / matita / lib / basics / jmeq.ma

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index 05c13498eff89c5dd4d4bd2559f0c860a49dd072..42e52c0a430a40ee20a133a2f23c283bff7b00e2 100644 (file)
--- 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.