def AP.len_take

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

import Base

1401# a list of n + m elements cut after n: n, then m elements
1402def AP.len_take(-T: Data, xs: List<&2, T>, n: Nat, -m: Nat, h: {List.length(&2, T, xs) == Nat.add(n, m) : Nat}) -> {List.length(&2, T, List.take(&2, T, xs, n)) == n : Nat}:
1403  match xs n:
1404    case Nil{} 0n:
1405      {==}
1406    case Nil{} 1n+p:
1407      Empty.absurd({List.length(&2, T, List.take(&2, T, Nil{}, 1n+p)) == 1n+p : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1408    case Con{x, t} 0n:
1409      {==}
1410    case Con{x, t} 1n+p:
1411      AP.succ_cong(List.length(&2, T, List.take(&2, T, t, p)), p, AP.len_take(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h)))