Lemma u : True.
Proof. exact I. Qed.