Goal forall A, A -> Type.
Proof.
  intros; eauto.
Qed.