def base_take_drop

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

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

235def base_take_drop(-A: Data, +xs: List<&2, A>, +k: Nat) -> {SC.append(A, List.take(&2, A, xs, k), List.drop(&2, A, xs, k)) == xs : List<&2, A>}:
236  match xs k:
237    case Nil{} _:
238      {==}
239    case Con{h, t} 0n:
240      {==}
241    case Con{+h, +t} 1n+p:
242      cons_cong(A, h, SC.append(A, List.take(&2, A, t, p), List.drop(&2, A, t, p)), t, base_take_drop(A, t, p))