∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w)
  (curr : ℕ) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (hidx : curr < w),
  InvImage (fun x1 x2 => x1 < x2)
    (fun x =>
      PSigma.casesOn x fun aig lhs =>
        PSigma.casesOn lhs fun lhs rhs =>
          PSigma.casesOn rhs fun rhs curr =>
            PSigma.casesOn curr fun curr hcurr =>
              PSigma.casesOn hcurr fun hcurr cin => PSigma.casesOn cin fun cin s => w - curr)
    ⟨(Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig
          { lhs := lhs.get curr hidx, rhs := rhs.get curr hidx, cin := cin }).aig,
      ⟨lhs.cast ⋯,
        ⟨rhs.cast ⋯,
          ⟨curr + 1,
            ⟨⋯,
              ⟨(Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig
                    { lhs := lhs.get curr hidx, rhs := rhs.get curr hidx, cin := cin }).cout,
                (s.cast ⋯).push
                  (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig
                      { lhs := lhs.get curr hidx, rhs := rhs.get curr hidx, cin := cin }).out⟩⟩⟩⟩⟩⟩
    ⟨aig, ⟨lhs, ⟨rhs, ⟨curr, ⟨hcurr, ⟨cin, s⟩⟩⟩⟩⟩⟩