case plus θ₁ θ₂ ih₁ ih₂ =>
  cases nv₁; case plus nv₁₁ nv₂₁ => cases nv₂; case plus nv₁₂ nv₂₂ =>
  apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ +ₛ θ₂)
⊢ nv₁ = nv₂
no goals