intro h _ _ _
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ t.Positive → ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
case mpr
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : t.Positive
i✝¹ : Fin 2
i✝ : Fin 1
a✝ : i✝ ∈ (![npow L n✝, bvar 0] i✝¹).term.bv
⊢ t.Positive