Consider disallowing body-less proofs that are not obligations

[utaal]

I think this, outside of a trait declaration should probably be disallowed:

proof fn a()
    requires true,
    ensures false;

It looks like a proof obligation.