[Agda] Short proof of falsity

[Anton Setzer]

> module strangeNat where
>
> data ℕ : Set where
> zero : ℕ → ℕ
> suc : ℕ → ℕ
>
> data ⊥ : Set where
>
> empty : ℕ → ⊥
> empty (zero y) = empty y
> empty (suc y) = empty y
>
> {-# BUILTIN NATURAL ℕ #-}
>
> p : ⊥
> p = empty 0


Anton and Karim