X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfdeq_length.ma;h=06fa93f19f9f5a060a779e24d7873b12b0f70a9f;hb=47a745462a714af9d65cea7b61af56524bd98fa1;hp=37a33504f98043e2c0fff67d3efa2aa20bbebb4e;hpb=6167cca50de37eba76a062537b24f7caef5b34f2;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index 37a33504f..06fa93f19 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -14,15 +14,19 @@ include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_length.ma". +include "basic_2/static/lfxs_fsle.ma". include "basic_2/static/lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) -(* Forward lemmas with length for local environments ************************) +(* Advanved properties with free variables inclusion ************************) -(* Basic_2A1: lleq_fwd_length *) -lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. -/2 width=3 by lfxs_fwd_length/ qed-. +lemma lfdeq_fsle_comp: ∀h,o. lfxs_fsle_compatible (cdeq h o). +#h #o #L1 #L2 #T * #f1 #Hf1 #HL12 +lapply (frees_lfdeq_conf h o … Hf1 … HL12) +lapply (lexs_fwd_length … HL12) +/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) +qed-. (* Properties with length for local environments ****************************) @@ -31,3 +35,10 @@ lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≛[h, o, T] ∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 → ∀U. ⬆*[f] T ≡ U → L1 ≛[h, o, U] L2. /3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-. + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: lleq_fwd_length *) +lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. +/2 width=3 by lfxs_fwd_length/ qed-. +