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