Goal forall x : nat, True.
  fix goal 1.
  assumption.
Fail Qed.
Undo.