- lfpxs based on tc_lfxs

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfdeq_length.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma
index d7c04b6ec3e919972b752958f6487ccc6d0ccb60..aafc792212195f92d80d600f689478cc581976fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma
@@ -19,5 +19,6 @@ include "basic_2/static/lfdeq.ma".
 
 (* Forward lemmas with length for local environments ************************)
 
+(* Basic_2A1: lleq_fwd_length *)
 lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → |L1| = |L2|.
 /2 width=3 by lfxs_fwd_length/ qed-.