# Pastebin Z4zjY2lD
data Suc (A : Set) : Set where
  zero : Suc A
  suc : A → Suc A

Fin : Nat → Set
Fin zero = False
Fin (suc n) = Suc (Fin n)