case S_axiom_neg nv₁ nv₂ p =>
  rw [NoVars.unique nv₁ nv₂] at p
  exact p rfl
nv₁ nv₂ : NoVars O
p : Sinf_const.eval (Sinf_const.coerce O nv₁) ≠ Sinf_const.eval (Sinf_const.coerce O nv₂)
⊢ False
no goals