rcases rel_uniq with ⟨y, ⟨hl, _⟩⟩
case intro
rel_sub : True
rel_uniq : ∃ x, 3 + 3 * x = 4 ∧ ∀ (y : ℤ), 3 + 3 * y = 4 → y = x
⊢ False
case intro.intro.intro
rel_sub : True
y : ℤ
hl : 3 + 3 * y = 4
right✝ : ∀ (y_1 : ℤ), 3 + 3 * y_1 = 4 → y_1 = y
⊢ False