def AP.take_drop

bend-osdev-array@0.1.0.1 · PROOF.bend:1370

import Base

1370def AP.take_drop(-T: Data, xs: List<&2, T>, n: Nat) -> {List.append(&2, T, List.take(&2, T, xs, n), List.drop(&2, T, xs, n)) == xs : List<&2, T>}:
1371  match xs n:
1372    case Nil{} _:
1373      {==}
1374    case Con{x, t} 0n:
1375      {==}
1376    case Con{x, t} 1n+p:
1377      AP.con_cong(T, x, List.append(&2, T, List.take(&2, T, t, p), List.drop(&2, T, t, p)), t, AP.take_drop(T, t, p))