X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_csx_vector.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_csx_vector.ma;h=c010a31a9eb17bb81ef61742ddb29c418596519d;hb=be2870b722324a1813ac9e72ebcb2cda6c8733d7;hp=fa81a32d258d33a03deccad8b99f39dc4629f6b1;hpb=0e3962b42f821bd7a2b30345a02488958d70fa2f;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index fa81a32d2..c010a31a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -41,7 +41,7 @@ lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⬆*[⫯i] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄. #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=11 by csx_inv_lifts, csx_lref_drops, drops_isuni_fwd_drop2/ +[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T