slight Ltac upgrades, more inbound...

Also, example 3 was stated incorrectly before… need to check if the
“success” in solving/proving it makes sense or if that was a
bug/loop-hole in the typing rules