- exclusion binder in local environments

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_csx_vector.ma

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 fa81a32d258d33a03deccad8b99f39dc4629f6b1..c010a31a9eb17bb81ef61742ddb29c418596519d 100644 (file)
--- 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