def AP.get_set_other

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

import Base

860def AP.get_set_other(-T: Data, xs: List<&2, T>, k1: Nat, k2: Nat, -v: T, h: {Nat.is_eq(k1, k2) == False{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k1, v), k2) == List.get(&2, T, xs, k2) : Maybe<&2, T>}:
861  match xs k1 k2:
862    case Nil{} _ _:
863      {==}
864    case Con{x, t} 0n 0n:
865      Empty.absurd({List.get(&2, T, List.set(&2, T, Con{x, t}, 0n, v), 0n) == List.get(&2, T, Con{x, t}, 0n) : Maybe<&2, T>}, AP.tf(h))
866    case Con{x, t} 0n 1n+q:
867      {==}
868    case Con{x, t} 1n+p 0n:
869      {==}
870    case Con{x, t} 1n+p 1n+q:
871      AP.get_set_other(T, t, p, q, v, h)