def g_zerosu

bend-osdev-bytes@0.1.1.0 · PROOF.bend:550

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

550def g_zerosu(+n: Nat, +acc: List<&2, U32>) -> {B.zeros.go(n, acc) == List.append(&2, U32, B.zeros(n), acc) : List<&2, U32>}:
551  match n:
552    case 0n:
553      {==}
554    case 1n+p:
555      Equal.trans(List<&2, U32>, B.zeros.go(p, Con{0, acc}), List.append(&2, U32, B.zeros(p), Con{0, acc}), Con{0, List.append(&2, U32, B.zeros(p), acc)},
556        g_zerosu(p, Con{0, acc}), zeros_consu(p, acc))