X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fgenv.ma;h=890126130ba9f041cfb407ce38cb75a359fd11ca;hb=caf822cbe34e204e6d1b72e272373b561c1a565a;hp=35365d802ca8d3d12a9007de834905e5d16ac715;hpb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma
index 35365d802..890126130 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma
@@ -44,7 +44,7 @@ lemma eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).
 #G1 elim G1 -G1 [| #G1 #I1 #T1 #IHG1 ] * [2,4: #G2 #I2 #T2 ]
 [3: /2 width=1 by or_introl/
 |2: elim (eq_bind2_dec I1 I2) #HI
-    [ elim (IHG1 G2) -IHG1 #HG 
+    [ elim (IHG1 G2) -IHG1 #HG
       [ elim (eq_term_dec T1 T2) #HT /2 width=1 by or_introl/ ]
     ]
 ]