Unfold function definition in auto-proofs

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).