import Base

def ap(h: (Nat -> Nat) -> Nat -> Nat, s: Nat -> Nat, n: Nat) -> Nat:
  h(s)(n)

def qof(f: (Nat -> Nat) -> Nat -> Nat) -> Quant:
  &1

def k(f: (Nat -> Nat) -> Nat -> Nat, g: Nat -> Nat, -A: Kind(qof(f)), b: Bool) -> Nat:
  match b:
    case True{}:
      ap(f, (x => x), 0n)
    case False{}:
      g(1n)

def main() -> Nat:
  k((y => y), (x => 5n), Unit, True{})