simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
  BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
  decide_eq_true_eq]
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ ⟦{ aig := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.aig,
        ref := (go aig (un (BVUnOp.shiftRightConst n✝) expr)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (un (BVUnOp.shiftRightConst n✝) expr)).getLsb idx
case un.shiftRightConst
w : Nat
assign : Assignment
w✝ : Nat
expr : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < w✝
n✝ : Nat
⊢ (eval assign expr).getLsb (n✝ + idx) = true → n✝ + idx < w✝