import Base

def ok() -> Nat:
  1n