def AP.get_app_l

bend-osdev-array@0.1.0.1 · PROOF.bend:828

import Base

828def AP.get_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.append(&2, T, xs, ys), k) == List.get(&2, T, xs, k) : Maybe<&2, T>}:
829  match xs k:
830    case Nil{} _:
831      Empty.absurd({List.get(&2, T, List.append(&2, T, Nil{}, ys), k) == List.get(&2, T, Nil{}, k) : Maybe<&2, T>}, AP.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 0n), True{}, Equal.sym(Bool, Nat.is_lt(k, 0n), False{}, AP.lt_zero(k)), h)))
832    case Con{x, t} 0n:
833      {==}
834    case Con{x, t} 1n+p:
835      AP.get_app_l(T, t, ys, p, h)