(* Advanced properties ******************************************************)
(* Basic_1: was only: sn3_appls_lref *)
-lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] →
+lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ →
∀Vs. L ⊢ ⬇* Vs → L ⊢ ⬇* ⒶVs.T.
#L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
lapply (csn_fwd_pair_sn … H) #HW1
lapply (csn_fwd_flat_dx … H) #H1
@csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
-elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
[ -H #H elim (H2 ?) -H2 //
| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
]
(* Basic_1: was: sn3_appls_cast *)
lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W →
∀Vs,T. L ⊢ ⬇* ⒶVs. T →
- L â\8a¢ â¬\87* â\92¶Vs. â\93£W. T.
+ L â\8a¢ â¬\87* â\92¶Vs. â\93\9dW. T.
#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
#V #Vs #IHV #T #H1T
lapply (csn_fwd_pair_sn … H1T) #HV