induction nv
θ : Sinf_term
nv : NoVars θ
⊢ Ø ⋁ θ =ₛ θ
case O
θ : Sinf_term
⊢ Ø ⋁ O =ₛ O

case S
θ t✝ : Sinf_term
a✝ : NoVars t✝
a_ih✝ : Ø ⋁ t✝ =ₛ t✝
⊢ Ø ⋁ t✝↗ =ₛ t✝↗

case plus
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
a_ih✝¹ : Ø ⋁ θ₁✝ =ₛ θ₁✝
a_ih✝ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ +ₛ θ₂✝ =ₛ θ₁✝ +ₛ θ₂✝

case times
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
a_ih✝¹ : Ø ⋁ θ₁✝ =ₛ θ₁✝
a_ih✝ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝