∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig),
  ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut aig input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧ ^^
      ⟦assign, { aig := aig, ref := input.cin }⟧)