двойное отрицание вставки в agda

Question

Я хочу некоторое уточнение о двойных отрицаниях в agda.

даже если

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

Я не могу понять, как доказать:

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

Который является длинная рука для ¬ (0 ≢ 0). Возможно, я пропустил идиому агды где-то на этом пути. Idealy Мне хотелось бы получить объяснение с минимальной ссылкой на стандартную библиотеку.

Answer 1

Вы можете доказать ¬¬z≡z по

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