λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
index 8ae0a99bec6b6407d8b6ff454012111427c3ed63..7f77340e77d8cdad5f3691b73373630967733587 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
@@ -62,7 +62,7 @@ lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
                        |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
 #L1 #L2 #n1 #n2 #H #HL
 elim (lveq_fwd_length … H) -H
->HL -HL /2 width=1 by conj/ 
+>HL -HL /2 width=1 by conj/
 qed-.
 
 lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →