induction θ <;> try contradiction
θ : Sinf_term
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
case O
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂

case S
a✝ : Sinf_term
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝↗)
⊢ nv₁ = nv₂

case plus
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ +ₛ a✝)
⊢ nv₁ = nv₂

case times
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ *ₛ a✝)
⊢ nv₁ = nv₂