update in binararies for λδ

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / grammar / lenv_append.ma

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 b741422cb0a6d5bdd41255a3d4e7f4bb28dc08a1..cd7a3d78885375d885bf72dcda054cda57cc3aaf 100644 (file)
--- 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.