double negation insertion in agda

Question

I want some clarification on double negations in agda.

even though

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

I cannot figure out how to prove:

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

Which is long hand for ¬ (0 ≢ 0). Perhaps I've missed an agda idiom somewhere along the way. Idealy I'd like an explanation with minimal reference the standard library.

Answer 1

You can prove ¬¬z≡z by

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