X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fllor_ldrop.ma;h=ef23ce14958995d196bf8f88887ec07883b4b945;hb=4720368dcf18593959c6d21484f62fb5b61f3d26;hp=5f82638e030bfb104cb2973d504cc1bfb71e4001;hpb=3da4aab04ff19ad3a96ce0a05f9ea6c45b58d92a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
index 5f82638e0..ef23ce149 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma
@@ -27,6 +27,7 @@ lapply (ldrop_fwd_length_lt2 … HLK1) -K1
 /5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/
 qed.
 
+(* Note: lemma 1400 concludes the "big tree" theorem *)
 lemma llor_total: ∀L1,L2,T,d. |L1| = |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
 #L1 @(lenv_ind_alt … L1) -L1
 [ #L2 #T #d #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/