Goal Type.
simpl; exact 0.
Abort.