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