closure ahead
Frankly everything you need to know about me should already be in the sidebar. Here, have some Agda instead:
{-# OPTIONS --sized-types #-}
open import Size
open import Data.Empty
data _<_ : Size → Size → Set where
lt : ∀ s → (r : Size< s) → r < s
data Acc (s : Size) : Set where
acc : (∀ {r} → r < s → Acc r) → Acc s
false : ⊥
false = ¬wf∞ (wf ∞) where
wf : ∀ s → Acc s
wf s = acc (λ {(lt .s r) → wf r})
¬wf∞ : Acc ∞ → ⊥
¬wf∞ (acc p) = ¬wf∞ (p (lt ∞ ∞))