{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data Nat = Z | S Nat

data Peano n where
	Zero :: Peano Z
	Succ :: Peano n -> Peano (S n)

type family Leq a b where
	Leq Z b = 'True
	Leq (S a) Z = False
	Leq (S a) (S b) = Leq a b

type family InRange a b x where
	InRange a b x = Leq a x '&& Leq x b


tall :: (InRange (S (S Z)) (S (S (S (S Z)))) n ~ 'True) => Peano n