PROOF.AP.set_app_l: def of bend-osdev-array@0.1.0.1
Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
Lines 844-851 of bend-osdev-array@0.1.0.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&start_line=844&end_line=851

import Base

def AP.set_app_l(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.set(&2, T, List.append(&2, T, xs, ys), k, v) == List.append(&2, T, List.set(&2, T, xs, k, v), ys) : List<&2, T>}:
  match xs k:
    case Nil{} _:
      Empty.absurd({List.set(&2, T, List.append(&2, T, Nil{}, ys), k, v) == List.append(&2, T, List.set(&2, T, Nil{}, k, v), ys) : List<&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)))
    case Con{x, t} 0n:
      {==}
    case Con{x, t} 1n+p:
      AP.con_cong(T, x, List.set(&2, T, List.append(&2, T, t, ys), p, v), List.append(&2, T, List.set(&2, T, t, p, v), ys), AP.set_app_l(T, t, ys, p, v, h))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.con_cong
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_zero