debugging example 2

example 2 is not passing automatically (all but 1 trivial goal, but the
environment in that goal is off slightly - it believes x is a bool when
it should be a number). I’ve looked over the related typing and proof
judgements and don’t see any obvious issues. I think it’s likely a poor
choice the automated tactic makes, but I’ll have to dissect it a little
further to see for sure.