Unfold function definition in auto-proofs

[joshlf]

Currently, our various auto-proof macros don't unfold the function body first, which severely limits what properties can be automatically proven (roughly, to statements which are vacuously true like trivial isValid definitions).