Axiom x : True.
Goal nat -> nat.
  intro x.
  abstract (exact x).
Qed.