def bitw.index_some

bend-osdev-algo@0.1.0.0 · PROOF.bend:453

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

453def bitw.index_some(m: Nat, -k: Nat, e: {A.bitw.index(m) == Some{k} : Maybe<&2, Nat>}) -> {m == 1n+k : Nat}:
454  match m:
455    case 0n:
456      Empty.absurd({0n == 1n+k : Nat}, absurd.ns(k, e))
457    case 1n+i:
458      %some_inj(i, k, e) : {1n+i == 1n+_ : Nat}
459      {==}