rcases rel_uniq with ⟨y, ⟨_, hrel⟩⟩
case intro
rel_sub : True
rel_uniq : ∃ x, x ^ 2 = 4 ∧ ∀ (y : ℝ), y ^ 2 = 4 → y = x
⊢ False
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
⊢ False