def len_append

bend-osdev-aead@0.1.0.0 · PROOF.bend:125

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

125def len_append(xs: List<&2, U32>, +ys: List<&2, U32>) -> {Nat.add(B.len(xs), B.len(ys)) == B.len(B.append(xs, ys)) : Nat}:
126  match xs:
127    case Nil{}:
128      {==}
129    case Con{h, t}:
130      %len_append(t, ys) : {1n+Nat.add(B.len(t), B.len(ys)) == 1n+_ : Nat}
131      {==}