(* Advanced forward lemmas **************************************************)
-lemma csn_fwd_applv: â\88\80L,T,Vs. L â\8a¢ â¬\87* â\92¶ Vs. T â\86\92 L â\8a¢ â¬\87* Vs â\88§ L â\8a¢ â¬\87* T.
+lemma csn_fwd_applv: â\88\80L,T,Vs. L â\8a¢ â¬\8a* â\92¶ Vs. T â\86\92 L â\8a¢ â¬\8a* Vs â\88§ L â\8a¢ â¬\8a* T.
#L #T #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHVs #HVs
lapply (csn_fwd_pair_sn … HVs) #HV