def AP.get_set_same
bend-osdev-array@0.1.0.1 · PROOF.bend:1484
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
1484def AP.get_set_same(-T: Data, xs: List<&2, T>, k: Nat, -v: T, h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}) -> {List.get(&2, T, List.set(&2, T, xs, k, v), k) == Some{v} : Maybe<&2, T>}:
1485 match xs k:
1486 case Nil{} _:
1487 Empty.absurd({List.get(&2, T, List.set(&2, T, Nil{}, k, v), k) == Some{v} : 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)))
1488 case Con{x, t} 0n:
1489 {==}
1490 case Con{x, t} 1n+p:
1491 AP.get_set_same(T, t, p, v, h)