ohadNov 3

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

Compositionality needs three cases though. :(

Show threadohadNov 3
Proof.
Show threadConstantine Theocharis

@ohad therapist: strength pentagon isn’t real, it can’t hurt you

strength pentagon:

Nov 3 at 2:58pmWeb
Show threadohadNov 3
@constantine The strength pentagon is your friend. Today's 'best practice' is to metaprogram these proofs and then check them.
Show threadConstantine TheocharisNov 3
@ohad That does sound much worse