Goal True.
  assert_succeeds (exact I).
  idtac.
  (* Error: No such goal. *)
Abort.