Nat.Lte
type (_, _) t =
| Z : ( z, 'a ) t
| S : ( 'n, 'm ) t -> ( 'n s, 'm s ) t
val refl : 'n nat -> ( 'n, 'n ) t
val trans : ( 'a, 'b ) t -> ( 'b, 'c ) t -> ( 'a, 'c ) t