def w8s_drop_app

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

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

208def w8s_drop_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) == ys : List<&2, B.OctByte>}:
209  match xs:
210    case Nil{}:
211      {==}
212    case Con{h, t}:
213      w8s_drop_app(t, ys)