def li.len_take

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:266

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

266def li.len_take(+n: Nat, +xs: List<&2, U32>) -> {Nat.is_le(n, B.len(xs)) == True{} : Bool} -> {B.len(B.take(n, xs)) == n : Nat}:
267  match n:
268    case 0n:
269      h => {==}
270    case 1n+p:
271      match xs:
272        case Nil{}:
273          h => bo.absurd({B.len(B.take(1n+p, Nil{})) == 1n+p : Nat}, h)
274        case Con{+x, +t}:
275          h => %li.len_take(p, t)(h) : {1n+B.len(B.take(p, t)) == 1n+_ : Nat}
276            {==}