agda中的双重否定插入

即使

z≡z : 0 ≡ 0 
z≡z = refl

我无法弄清楚如何证明：

¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥ 
¬¬z≡z ?

这是长手¬ (0 ≢ 0)。也许我错过了一路上某处agda的成语。理想情况下，我想用最少的参考来解释标准库。

2013-08-30 user833970

您可以通过

¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥ 
¬¬z≡z h = h refl

证明 ¬¬z≡z

2013-08-30 05:03:27 asr

回答