Reasoning about higher-order program transformation?

Thanks for the insighful answer @Lyxia! I have two follow-up questions:

Wouldn’t this approach just shift the “continuation induction” stuff that you explained above to the auxiliary lemmas about subst?

Nice. Assuming one switches to using this monad, would that simplify the proof or one would have to perform “continuation induction” as above but for bind this time?

Thanks!
Nicolás