def off.ldrop_drop

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

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

1014def off.ldrop_drop(+j: Nat, +i: Nat, xs: List<&2, U32>) -> {B.drop(i, B.drop(j, xs)) == B.drop(Nat.add(j, i), xs) : List<&2, U32>}:
1015  match j xs:
1016    case 0n _:
1017      {==}
1018    case 1n+q Nil{}:
1019      off.ldrop_nil(i)
1020    case 1n+q Con{x, t}:
1021      off.ldrop_drop(q, i, t)