module Nat;

builtin nat
type Nat :=
  | zero : Nat
  | suc : Nat → Nat;