rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
case S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝
case S_axiom.S_axiom
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁₁ nv₁₂ : NoVars θ₁✝
e₁ : Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₁) = Sinf_const.eval (Sinf_const.coerce θ₁✝ nv₁₂)
nv₂₁ nv₂₂ : NoVars θ₂✝
e₂ : Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₁) = Sinf_const.eval (Sinf_const.coerce θ₂✝ nv₂₂)
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝