X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Fcpx%2Fcpx_length.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Fcpx%2Fcpx_length.etc;h=c769990b2050a85575d8020e8ed0e42f28656088;hb=7e80b8d7a4b2c38729512dee28b3e0ecf9595c2a;hp=0000000000000000000000000000000000000000;hpb=a145b5df4a86b3d5f8516a9c1cb76a62f6327151;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc
new file mode 100644
index 000000000..c769990b2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc
@@ -0,0 +1 @@
+lemma cpx_inv_lref1_ge: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → |L| ≤ i → T2 = #i.