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

State before:
L : Language
inst✝¹ : Operator.One L
inst✝ : Operator.Mul L
n : ℕ
⊢ npow L (n + 1) = op(*).comp ![npow L n, bvar 0]
Tactic:
simp [npow, foldr]
State after:
no goals