case times nv₁ nv₂ =>
  rcases nv₁ with ⟨nv₁₁, nv₁₂, e₁⟩
  rcases nv₂ with ⟨nv₂₁, nv₂₂, e₂⟩
  constructor <;> try constructor <;> try assumption
θ θ₁✝ θ₂✝ : Sinf_term
a✝¹ : NoVars θ₁✝
a✝ : NoVars θ₂✝
nv₁ : Ø ⋁ θ₁✝ =ₛ θ₁✝
nv₂ : Ø ⋁ θ₂✝ =ₛ θ₂✝
⊢ Ø ⋁ θ₁✝ *ₛ θ₂✝ =ₛ θ₁✝ *ₛ θ₂✝
no goals