1 2 3 4
Require Import Equality. Theorem foo (u : unit) (H : u = u) : True. dependent destruction H. Abort.
