def bq.len_take

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:435

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U

435def bq.len_take(xs: List<&2, U32>, k: Nat, h: {Nat.is_le(k, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.length(&2, U32, List.take(&2, U32, xs, k)) == k : Nat}:
436  match xs k:
437    case Nil{} 0n:
438      {==}
439    case Nil{} 1n+kp:
440      Empty.absurd({0n == 1n+kp : Nat}, bq.ft(h))
441    case Con{x, t} 0n:
442      {==}
443    case Con{x, t} 1n+kp:
444      U.uq.succ_cong(List.length(&2, U32, List.take(&2, U32, t, kp)), kp, bq.len_take(t, kp, h))