Nat.Adds
type ('a, 'b, 'c) t =
| Z : ( z, 'n, 'n ) t
| S : ( 'a, 'b, 'c ) t -> ( 'a s, 'b, 'c s ) t
val add_zr : 'n nat -> ( 'n, z, 'n ) t