Theorem simple : forall A, A -> A.
Proof.
auto.
Qed.