case S_axiom nv₂' nv₃ e' =>
  constructor <;> try assumption
  rw [NoVars.unique nv₂ nv₂'] at e
  exact (Eq.trans e e')
θ₁ θ₂ θ₃ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
nv₂' : NoVars θ₂
nv₃ : NoVars θ₃
e' : Sinf_const.eval (Sinf_const.coerce θ₂ nv₂') = Sinf_const.eval (Sinf_const.coerce θ₃ nv₃)
⊢ Δ ⋁ θ₁ =ₛ θ₃
no goals