Theorem: LO.FirstOrder.Semiterm.Operator.Exp.positive_iff (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
ξ : Type u_1
n : ℕ
inst✝ : L.Exp
t : Semiterm L ξ (n + 1)
⊢ (exp.operator ![t]).Positive ↔ t.Positive
Tactic:
simp [positive_operator_iff, Exp.term_eq, bv_func]
State after:
no goals