data Nat = Z | S Nat
 --deriving Eq

instance Eq Nat where
  x == y = True
{-
  Z   == Z   = True
  S m == S n = m == n
  Z   == S _ = False
  S _ == Z   = False
-}

-- Equality is needed, e.g., for list membership:
member :: Eq a => a -> [a] -> Bool
member x [] = False
member x (y:ys) = x == y || member x ys


-- Data type for "uniquely indexed" complex values::
data IVal a = IVal Int a

-- Equality is defined by comparing the index only:
instance Eq a => Eq (IVal a) where
  IVal i1 _ == IVal i2 _ = i1 == i2


-- Last element of a list:
last :: Data a => [a] -> a
last xs | xs === _ ++ [x] = x   where x free


-- Addition on natural numbers:
add :: Nat -> Nat -> Nat
add Z  n    = n
add (S m) n = S (add m n)

-- Not allowed:
-- hoVar = x True  where x free

solve' :: Bool -> Bool
solve' True = True