Goal True.
pose proof 0 as n.
Fail apply pair in n.
(* Used to be an anomaly for a while *)