simp [bvar]
L : Language
ξ : Type u_1
n : ℕ
inst✝ : Operator.One L
k : L.Mul
t : Semiterm L ξ (n + 1)
n✝ : ℕ
h : ∀ (i : Fin 2), ∀ i_1 ∈ (![npow L n✝, bvar 0] i).term.bv, t.Positive
⊢ 0 ∈ (![npow L n✝, bvar 0] 1).term.bv
no goals