Мне нужны пояснения по поводу двойных отрицаний в agda.
Несмотря на то
z≡z : 0 ≡ 0
z≡z = refl
Не могу понять, как доказать:
¬¬z≡z : (0 ≡ 0 → ⊥) → ⊥
¬¬z≡z ?
Это длинная рука для ¬ (0 ≢ 0). Возможно, я где-то пропустил идиому agda. В идеале я хотел бы получить объяснение с минимальной ссылкой на стандартную библиотеку.
