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