Mastodawn

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

Compositionality needs three cases though. :(

Proof.

@ohad I have pet peeves about commutative diagrams and which of them deserve the name proof.

You have managed to not trigger them. Bravo.

@JacquesC2 details please?

@ohad private message incoming. I don't want to start a flame war.

You just did by declaring this a private conversation.

@MartinEscardo @ohad It'll be fun to watch, given how very little information there is to use to 'flame' on.