我知道排除中间在构造逻辑中是不可能的。然而，当我尝试在 Coq 中展示它时，我陷入了困境。
Theorem em: forall P : Prop, ~P \/ P -> False.
我的做法是：
intros P H.
unfold not in H.
intuition.
系统说如下：
2 subgoals
P : Prop
H0 : P -> False
______________________________________(1/2)
False
______________________________________(2/2)
False
我应该如何进行？谢谢