Underspecified checking of lambda-abstractions

Right now, the kernel accepts terms as such as :

fun A: Prop, x : A, y : x => y

While it would be fun to have such weird feature if we did set theory, the fact that it gets accepted here is a bug in _infer, which should check that the types given in binders of lambda-abstractions live in universes.