∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (n : ℕ) (input : aig.RefVec w)
  (curr : ℕ) (hcurr : curr ≤ n) (s : aig.RefVec (w * curr)) (h : curr < n),
  InvImage (fun x1 x2 => x1 < x2)
    (fun x => PSigma.casesOn x fun curr hcurr => PSigma.casesOn hcurr fun hcurr s => n - curr)
    ⟨curr + 1, ⟨⋯, s.append input⟩⟩ ⟨curr, ⟨hcurr, s⟩⟩