Prove dozens of syntactic substitution lemmata in one fell swoop with an induction principle with only two cases? Check.

Compositionality needs three cases though. :(