apply congrArg₂
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times nv₁₂ nv₂₂
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂