cases op with
| and =>
  simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
    BitVec.getLsb_and]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| or =>
  simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
    BitVec.getLsb_or]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| xor =>
  simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
    BitVec.getLsb_xor]
  simp only [go_val_eq_bitblast, RefStream.getRef_cast]
  rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
  rw [← go_val_eq_bitblast]
  rw [lih]
| add =>
  simp only [go, eval_bin, BVBinOp.eval_add]
  apply blastAdd_eq_eval_getLsb
  . intros
    dsimp
    rw [go_denote_mem_prefix]
    rw [← lih (aig := aig)]
    . simp
    . assumption
    . simp [Ref.hgate]
  . intros
    rw [← rih]
case bin
w : Nat
assign : Assignment
w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
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 := (go aig (lhs.bin op rhs)).val.aig, ref := (go aig (lhs.bin op rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin op rhs)).getLsb idx
no goals