subtype universe constraint problem

Stream: new members

[Somo S.]

Why is it not possible to state the following theorem. Even though all terms involved are (or should be) well defined:

example : (Subtype fun (a, b) => 5 ≤ a + b) = (Subtype fun (a, b) => 5 ≤ a + b) := rfl
-- ERROR^^: stuck at solving universe constraint max 2 (?u.3+1) =?= max 2 (?u.11+1)

#reduce (Subtype fun (a, b) => 5 ≤ a + b) -- ok
#check (Subtype fun (a, b) => 5 ≤ a + b)  -- ok

how does one resolve the universe constraint problem?

[Damiano Testa]

This is probably some unification order. This works:

theorem subt_eq_self :  (Subtype (α := Nat × Nat) fun (a, b) => 5 ≤ a + b) = (Subtype fun (a, b) => 5 ≤ a + b) := rfl