Remove Universe Level Erasure

[marcusrossel]

Universe level erasure doesn't work. E.g. if we take the theorem ∀ (a : Nat), ULift.down (ULift.up a) = a then with universe level erasure we can apply it in both directions. If we now obtain a proof of 10 = 10 like:

(1) 10
(2) ULift.down (ULift.up 10)
(3) 10

... then we will instantiate the universe params in (2) using mvars. But the first of these params will never be resolved, as the expression 10 only resolves the second one to 0.