TODO: Need to do the same for the stack proof.
TODO: Unfolding should be automatic.