不使用经典逻辑证明¬(p ↔ ¬p)

目前为止见过的最难的，最不容易想到的题目

关键点

因为不能使用经典逻辑，所以不能使用排中律，既不能构造出p ∨ ¬p类型，然后使用Or.elim分类讨论，这题其实只要能构造出一个p类型就很好解决了，所以关键就是怎么弄出p。

解决方法

还是跟我上一篇文章一样，我总是会忽略一个东西，¬p的定义是p → False，所以这题的切入点其实是构造一个p → False，在构造它的时候我们可以先在函数中弄出p了。有了¬p再根据题目条件很容易就能得到p，下面看代码

example : ¬(p ↔ ¬p) :=
  fun h:p ↔ ¬p =>
    have nhp:¬p := fun hp:p => absurd hp (h.mp hp)
    have hp:p := h.mpr nhp
    absurd hp nhp