simp [Operator.foldr]
case succ
L : Language
hz✝ : Operator.Zero L
ho : Operator.One L
ha : Operator.Add L
z : ℕ
hz : z + 1 ≠ 0
⊢ op(+).foldr op(1) (List.replicate (z + 1) op(1)) =
    op(+).comp
      ![match z + 1 with
        | 0 => op(0)
        | n.succ => op(+).foldr op(1) (List.replicate n op(1)),
        op(1)]
no goals