def AP.len_drop
bend-osdev-array@0.1.0.1 · PROOF.bend:1413
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
1413def AP.len_drop(-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.drop(&2, T, xs, n)) == m : Nat}:
1414 match xs n:
1415 case Nil{} 0n:
1416 h
1417 case Nil{} 1n+p:
1418 Empty.absurd({List.length(&2, T, List.drop(&2, T, Nil{}, 1n+p)) == m : Nat}, AP.sz(Nat.add(p, m), Equal.sym(Nat, 0n, 1n+Nat.add(p, m), h)))
1419 case Con{x, t} 0n:
1420 h
1421 case Con{x, t} 1n+p:
1422 AP.len_drop(T, t, p, m, AP.pred_cong(List.length(&2, T, t), Nat.add(p, m), h))