∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w)
  (curr : ℕ) (cin : aig.Ref) (hidx : curr < w),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig
            { lhs := lhs.get curr hidx, rhs := rhs.get curr hidx, cin := cin }).aig.decls.size