∀ {α : Type u_2} {β : Type u_1} (as : Array α) (i : ℕ) (bs : Array β),
  i < as.size →
    ∀ (__do_lift : β),
      InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun i bs => as.size - i) ⟨i + 1, bs.push __do_lift⟩
        ⟨i, bs⟩