cases k <;> simp [positive_operator_iff, operator_comp, npow_zero, npow_succ]
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
k : ℕ
⊢ ((npow L k).operator ![t]).Positive ↔ k = 0 ∨ t.Positive
case succ
L : Language
ξ : Type u_1
n : ℕ
inst✝¹ : Operator.One L
inst✝ : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
⊢ (∀ i ∈ op(*).term.bv, ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive) ↔ t.Positive