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