Nat.N5
type 'a plus_n = 'a N4.plus_n s
type n = z plus_n
val eq : ( n, n ) Base.Type_equal.t
val n : z plus_n nat
val add : 'm nat -> 'm plus_n nat * ( z plus_n, 'm, 'm plus_n ) Adds.t