Make assert_smaller : a -> b -> b

Allow second argument of assert_smaller to be of different type than first argument since this could be useful for functions that arewritten with Universe-style pattern matching, i.e., where the rhs
pattern has different type than the lhs expression.