X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Ffsubst_lift.ma;h=ad0de7230e87c803d0aade06d7b13f53738f9ab3;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hp=c9d6560286a32f854e2577852c8a4b6e261e9811;hpb=cfd201c62dd9b854bfb4ada648d3e556b29fac3a;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma index c9d656028..ad0de7230 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma @@ -13,44 +13,39 @@ (**************************************************************************) include "delayed_updating/substitution/fsubst.ma". -include "delayed_updating/substitution/lift_prototerm.ma". -include "delayed_updating/substitution/lift_structure.ma". -include "delayed_updating/syntax/preterm.ma". -include "delayed_updating/syntax/prototerm_proper.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". (* FOCALIZED SUBSTITUTION ***************************************************) -lemma lift_fsubst_sn (f) (t) (u) (p): Ꝕu → p ⧸ϵ t → - (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]). -#f #t #u #p #Hu #Hp #ql * * +(* Constructions with lift for preterm **************************************) + +lemma lift_term_fsubst_sn (f) (t) (u) (p): + (🠡[f]t)[⋔(🠡[f]p)←🠡[🠢[f]p]u] ⊆ 🠡[f](t[⋔p←u]). +#f #t #u #p #ql * * [ #rl * #r #Hr #H1 #H2 destruct - >lift_append_proper_dx - /4 width=1 by subset_in_ext_f1_dx, or_introl/ + >lift_path_append + /4 width=3 by in_comp_lift_path_term, or_introl, ex2_intro/ | * #q #Hq #H1 #H0 - @(ex2_intro … H1) @or_intror @conj // - #r #H2 destruct - @H0 -H0 [|