def w8s_len_app

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

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

215def w8s_len_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys)) : Nat}:
216  match xs:
217    case Nil{}:
218      {==}
219    case Con{h, t}:
220      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, List.append(&2, B.OctByte, t, ys)), Nat.add(List.length(&2, B.OctByte, t), List.length(&2, B.OctByte, ys)), w8s_len_app(t, ys))