# Pastebin IxTZjTl5
open import Agda.Builtin.Nat

data Fin : Nat -> Set where
 zero : {n : Nat} -> Fin (suc n)
 succ : {n : Nat} -> Fin n -> Fin (suc n)

data False : Set where
record True : Set where constructor tt

¬Fin0 : Fin 0 → False
¬Fin0 ()

Fin-elim : (P : ∀ {n} → Fin n → Set)
  (zero* : ∀ {n} → P (zero {n}))
  (succ* : ∀ {n} {i : Fin n} → P i → P (succ i))
  → ∀ {n} (i : Fin n) → P i
Fin-elim P zero* succ* zero = zero*
Fin-elim P zero* succ* (succ i) = succ* (Fin-elim P zero* succ* i)

expl : ∀ {A} → Fin 0 → A
expl {A} = Fin-elim (λ { {zero} i → A ; {suc n} i → True }) _ _

¬Fin0' : Fin 0 → False
¬Fin0' = expl