def off.lat_take

bend-osdev-bytes@0.1.1.0 · PROOF.bend:1023

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

1023def off.lat_take(+i: Nat, +n: Nat, xs: List<&2, U32>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>}:
1024  match i n xs:
1025    case 0n 0n _:
1026      h => off.no({B.at(Nil{}, 0n) == B.at(xs, 0n) : Maybe<&2, U32>}, h)
1027    case 1n+p 0n _:
1028      h => off.no({B.at(Nil{}, 1n+p) == B.at(xs, 1n+p) : Maybe<&2, U32>}, h)
1029    case 0n 1n+q Nil{}:
1030      h => {==}
1031    case 0n 1n+q Con{x, t}:
1032      h => {==}
1033    case 1n+p 1n+q Nil{}:
1034      h => {==}
1035    case 1n+p 1n+q Con{x, t}:
1036      h => off.lat_take(p, q, t, h)