λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / genv.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/genv.ma
index 35365d802ca8d3d12a9007de834905e5d16ac715..890126130ba9f041cfb407ce38cb75a359fd11ca 100644 (file)
--- 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/ ]
     ]
 ]