exact ⟨by intro h; exact ⟨h 0, h 1⟩,
  by intro h i; cases i using Fin.cases <;> simp [Fin.eq_zero, *]⟩
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Mul
t u : Semiterm L ξ (n + 1)
⊢ (∀ (i : Fin 2), (![t, u] i).Positive) ↔ t.Positive ∧ u.Positive
no goals