type Nat : Type

free type Nat ::= Zero | Suc (Prec : Nat)