X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fllor%2Flleq_llor.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fllor%2Flleq_llor.etc;h=a180d112442c6f9c620d036acec1f5a3a911f0a9;hb=dffdece065d12d9961a6c3f1222f6d112030336f;hp=0000000000000000000000000000000000000000;hpb=87fbbf33fcc2ed91cc8b8a08e1c378ef49ac723d;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc new file mode 100644 index 000000000..a180d1124 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/llor.ma". +include "basic_2/substitution/lleq_alt.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Properties on poinwise union for local environments **********************) + +lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L. +#T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct +#HL1 #IHT @lleq_intro_alt // +#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) +#Hi elim (ldrop_O1_lt L1 i) // +#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2