]
qed.
-lemma csx_applv_delta: â\88\80h,g,I,G,L,K,V1,i. â\87©[i] L ≡ K.ⓑ{I}V1 →
- â\88\80V2. â\87§[0, i + 1] V1 ≡ V2 →
+lemma csx_applv_delta: â\88\80h,g,I,G,L,K,V1,i. â¬\87[i] L ≡ K.ⓑ{I}V1 →
+ â\88\80V2. â¬\86[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, drop_fwd_drop2/
qed.
(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta: â\88\80h,g,a,G,L,V1s,V2s. â\87§[0, 1] V1s ≡ V2s →
+lemma csx_applv_theta: â\88\80h,g,a,G,L,V1s,V2s. â¬\86[0, 1] V1s ≡ V2s →
∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
theorem csx_gcr: ∀h,g. gcr (cpx h g) (eq …) (csx h g) (csx h g).
#h #g @mk_gcr //
-[ /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/
+[ /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=7 by csx_applv_delta/
| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
@(csx_applv_theta … HV12s) -HV12s