def off.ldrop_app_add

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

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

989def off.ldrop_app_add(a: List<&2, U32>, +n: Nat, +b: List<&2, U32>) -> {B.drop(Nat.add(B.len(a), n), B.append(a, b)) == B.drop(n, b) : List<&2, U32>}:
990  match a:
991    case Nil{}:
992      {==}
993    case Con{h, t}:
994      off.ldrop_app_add(t, n, b)