simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
  BitVec.getLsb_xor]
case bin.xor
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 := (go aig (lhs.bin BVBinOp.xor rhs)).val.aig,
        ref := (go aig (lhs.bin BVBinOp.xor rhs)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (lhs.bin BVBinOp.xor rhs)).getLsb idx
case bin.xor
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✝
⊢ xor
      ⟦{ aig := (go (go aig lhs).1.aig rhs).1.aig, ref := ((go aig lhs).1.stream.cast ⋯).getRef idx hidx },
        assign.toAIGAssignment⟧
      ((eval assign rhs).getLsb idx) =
    xor ((eval assign lhs).getLsb idx) ((eval assign rhs).getLsb idx)