{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MonoLocalBinds #-}

import Data.Kind(Type)

data And (a :: Type) (b :: Type) = MkAnd a b
data Nat

z :: Nat
z = undefined

s :: Nat -> Nat
s = undefined



ind :: (forall (p :: (Nat -> Type)). (
  (p z) ->
  (forall (x :: Nat). (p x -> p (s x))) ->
  (forall (x :: Nat). p x)
  ))
ind = undefined

-- a :: forall (zz :: Nat) (x :: Nat -> Type). x zz -> x zz
-- a = undefined

main :: IO ()
main = return ()