+(* Basic_1: was: sn3_appls_beta *)
+lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W →
+ ∀Vs,V,T. L ⊢ ⬇* ⒶVs.ⓓV.T →
+ L ⊢ ⬇* ⒶVs. ⓐV.ⓛW. T.
+#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
+#V0 #Vs #IHV #V #T #H1T
+lapply (csn_fwd_pair_sn … H1T) #HV0
+lapply (csn_fwd_flat_dx … H1T) #H2T
+@csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T
+[ #X #H #H0
+ elim (cprs_fwd_beta_vector … H) -H #H
+ [ -H1T elim (H0 ?) -H0 //
+ | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+ ]
+| -H1T elim Vs -Vs //
+]
+qed.
+
+(* Basic_1: was: sn3_appls_abbr *)