simp only [go, blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
  eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
  Bool.and_iff_right_iff_imp, decide_eq_true_eq]
case zeroExtend
w : Nat
assign : Assignment
w✝ v : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
⊢ ⟦{ aig := (go aig (zeroExtend v inner)).val.aig, ref := (go aig (zeroExtend v inner)).val.stream.getRef idx hidx },
      assign.toAIGAssignment⟧ =
    (eval assign (zeroExtend v inner)).getLsb idx
case zeroExtend
w : Nat
assign : Assignment
w✝ v : Nat
inner : BVExpr w✝
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (go aig inner).val.aig, ref := (go aig inner).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign inner).getLsb idx
aig : AIG BVBit
idx : Nat
hidx : idx < v
⊢ (eval assign inner).getLsb idx = true → idx < w✝