. rw [← hleft idx hidx]
  rw [← hright idx hidx]
  unfold blastAdd
  dsimp
  rw [blastAdd.go_eq_eval_getLsb _ 0 (by omega) _ _ _ _ assign lhs rhs _ _]
  . simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast', BinaryRefStream.rhs_getRef_cast]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . simp
  . omega
  . intros
    simp only [BinaryRefStream.lhs_getRef_cast, Ref_cast']
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [hleft]
  . intros
    simp only [BinaryRefStream.rhs_getRef_cast, Ref_cast']
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    rw [hright]
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (blastAdd aig input).aig, ref := (blastAdd aig input).stream.getRef idx hidx }, assign⟧ =
    (lhs.getLsb idx).xor ((rhs.getLsb idx).xor (BitVec.carry idx lhs rhs false))

case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ idx < w
case i_lt
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
assign : α → Bool
input : aig.BinaryRefStream w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ idx < w