def length_drop

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:255

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

255def length_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.length(A, List.drop(&2, A, xs, k)) == Nat.sub(SC.length(A, xs), k) : Nat}:
256  match xs k:
257    case Nil{} 0n:
258      {==}
259    case Nil{} 1n+p:
260      {==}
261    case Con{x, t} 0n:
262      {==}
263    case Con{x, +t} 1n+p:
264      length_drop(A, t, p)