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 TheocharisNov 3

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

strength pentagon:

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