1 2 3 4 5 6 7 8 9 10
Lemma H : Prop = Prop. reflexivity. Qed. Lemma foo : match H in (_ = X) return X with | eq_refl => True end. Proof. Fail destruct H. Abort.