import Base

def thm(x: Nat) -> Nat:
  x