apply blastAdd_eq_eval_getLsb
case bin.add
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ⟦{
        aig :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
              { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).aig,
        ref :=
          (blastAdd (go (go aig lhs).1.aig rhs).1.aig
                  { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign lhs + eval assign rhs).getLsb idx
case bin.add.hleft
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.lhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx

case bin.add.hright
w : Nat
assign : Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig lhs).val.aig, ref := (go aig lhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign lhs).getLsb idx
rih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig rhs).val.aig, ref := (go aig rhs).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig,
          ref :=
            { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }.rhs.getRef idx hidx },
        assign.toAIGAssignment⟧ =
      (eval assign rhs).getLsb idx