(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
+lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
∀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
]
qed.
-theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
+theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g).
#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.