def li.len_take

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:165

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

165def 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}:
166  match n:
167    case 0n:
168      h => {==}
169    case 1n+p:
170      match xs:
171        case Nil{}:
172          h => bo.absurd({B.len(B.take(1n+p, Nil{})) == 1n+p : Nat}, h)
173        case Con{+x, +t}:
174          h => %li.len_take(p, t)(h) : {1n+B.len(B.take(p, t)) == 1n+_ : Nat}
175            {==}