free type Nat ::= Zero | Suc (prec : Nat)
op f(x:Nat):Nat = Suc x