def q_at_app_lt

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

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

1250def q_at_app_lt(+i: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.w8s.at(B.w8s.drop(i, B.w8s.append.fast(xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
1251  %F_app(xs, ys) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}
1252  off.at_app_lt(i, xs, ys, h)