dan on Nostr: also if you have some underlying shape (like a tree) you're proving things about, you ...

also if you have some underlying shape (like a tree) you're proving things about, you better create some reusable machinery for induction. otherwise it'll happily write every induction from scratch at every level of the proof and then get completely lost in the cases