X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fgrammar%2Flenv_append.ma;h=cd7a3d78885375d885bf72dcda054cda57cc3aaf;hp=b741422cb0a6d5bdd41255a3d4e7f4bb28dc08a1;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hpb=3a4509b8e569181979f5b15808361c83eb1ae49a

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma
index b741422cb..cd7a3d788 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma
@@ -57,7 +57,6 @@ lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = |L| + 1.
 #I #L #V >append_length //
 qed.
 
-(* Basic_1: was just: chead_ctail *)
 lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
 #L elim L -L /2 width=5 by ex2_3_intro/
 #L #Z #X #IHL #I #V elim (IHL Z X) -IHL
@@ -122,7 +121,6 @@ qed-.
 
 (* Basic eliminators ********************************************************)
 
-(* Basic_1: was: c_tail_ind *)
 lemma lenv_ind_alt: ∀R:predicate lenv.
                     R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
                     ∀L. R L.