∀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
∀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