[Bug]: Each different sort universe must be translated to a unique type universe at the smt level

We are wrongly unifying sorts of different universe at the smt level. Indeed, this does not preserve Lean4 semantics and therefore can lead to false positive results.

E.g.
```
theorem sort_unification_thm1 :
(∀ (x : β) (f : β → Nat), f x > 10) →
(∀ (α : Type) (x : α) (f : α → Nat), f x > 10) := by sorry

#solve [sort_unification_thm1]

theorem sort_unification_thm2 :
(∀ (β : Type u) (x : β) (f : β → Nat), f x > 10) →
(∀ (α : Type v) (x : α) (f : α → Nat), f x > 10) := by sorry

#solve [sort_unification_thm2]

```
These two theorems are wrongly declared as `Valid` while we can't derive a proof a the Lean4 level.
For the first case, β has `Type u` while α has `Type 1`.
For the second case, β has `Type u + 1` while α has `Type v + 1`.

We therefore can't instantiate the hypothesis to conclude.