Theorem identity (n : nat) : n = n.
Proof.
  reflexivity.
Qed.