def AP.get_rep
bend-osdev-array@0.1.0.1 · PROOF.bend:1493
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
1493def AP.get_rep(-T: Data, n: Nat, k: Nat, +v: T, h: {Nat.is_lt(k, n) == True{} : Bool}) -> {List.get(&2, T, List.replicate(T, n, v), k) == Some{v} : Maybe<&2, T>}:
1494 match n k:
1495 case 0n _:
1496 Empty.absurd({List.get(&2, T, List.replicate(T, 0n, 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)))
1497 case 1n+p 0n:
1498 {==}
1499 case 1n+p 1n+q:
1500 AP.get_rep(T, p, q, v, h)