Jon Sterling on Nostr: I also feel that all this knowledge is kind of outdated now that you can use a proof ...

I also feel that all this knowledge is kind of outdated now that you can use a proof assistant or a programming language to get a *direct* “synthetic” notion of derivation tree, for which structural induction is the definitional principle rather than something you prove in some complicated and irrelevant way.