Theorem t: True.
Fail destruct 0 as x.