∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ /4 width=12 by csx_inv_lift, csx_lref_bind, ldrop_fwd_drop2/
+[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
#h #g @mk_acr //
-[ /3 width=1 by csx_applv_cnx/
-|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
+[ /2 width=8 by csx_lift/
+| /3 width=1 by csx_applv_cnx/
+|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
| /2 width=7 by csx_applv_delta/
| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
@(csx_applv_theta … HV12s) -HV12s
@csx_abbr //
-| /2 width=8 by csx_lift/
]
qed.