def li.mask_drop

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:220

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

220def li.mask_drop(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.drop(n, xs)) == B.drop(n, B.mask(xs)) : List<&2, U32>}:
221  match n:
222    case 0n:
223      {==}
224    case 1n+p:
225      match xs:
226        case Nil{}:
227          {==}
228        case Con{+h, +t}:
229          li.mask_drop(p, t)