rw [NoVars.unique nv₁ nv₂] at p
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₁) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₂) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False