feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes #217
feat(frontends/lean): coercion num -> int even when nat is not open, closes #219

I also had to mark the coercions as reducible.
Otherwise, given the constraint

          ?M (int.of_num 0) =?= (int.of_nat (nat.to_nat 0))

the unifier will not generate the solution

          ?M := fun x, x
feat(frontends/lean): coercion num -> int even when nat is not open, closes #219