have htwo := hrel (2) (by ring_nf)
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
⊢ False
case intro.intro.intro
rel_sub : True
y : ℝ
left✝ : y ^ 2 = 4
hrel : ∀ (y_1 : ℝ), y_1 ^ 2 = 4 → y_1 = y
htwo : 2 = y
⊢ False