相关疑难解决方法(0)

我试图从一个排除中间的在线课程中证明以下简单定理是无可辩驳的,但在第1步被卡住了:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

现在我得到:

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

如果我apply H,那么目标就是P \/ ~P,中间被排除在外,无法建设性地证明.但除此之外apply,我不知道可以对假设做些什么P \/ (P -> False) -> False:暗示->是原始的,我不知道如何destruct分解它.这是唯一的假设.

我的问题是,如何使用原始策略(如此处所表征,即没有神秘auto的策略)来证明这一点？

谢谢.