def li.len_drop

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

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

251def li.len_drop(+n: Nat, +xs: List<&2, U32>) -> {B.len(B.drop(n, xs)) == Nat.sub(B.len(xs), n) : Nat}:
252  match n:
253    case 0n:
254      match xs:
255        case Nil{}:
256          {==}
257        case Con{+h, +t}:
258          {==}
259    case 1n+p:
260      match xs:
261        case Nil{}:
262          {==}
263        case Con{+h, +t}:
264          li.len_drop(p, t)