. rw [← hgo]
  simp only [eval_signExtend]
  rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
  . simp only [blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
      BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
      decide_eq_true_eq]
    apply BitVec.lt_of_getLsb
  . subst heq
    rw [BitVec.msb_zero_length]
case signExtend.inl
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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
res : RefStreamEntry BVBit v
hgo : blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx

case signExtend.inl.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ { w := originalWidth, stream := (go aig inner).1.stream }.w = 0
case signExtend.inl.htarget
w : Nat
assign : Assignment
originalWidth v : Nat
inner : BVExpr originalWidth
ih :
  ∀ (aig : AIG BVBit) (idx : Nat) (hidx : idx < originalWidth),
    ⟦{ 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
res : RefStreamEntry BVBit v
hgo : blastSignExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream } = res
this : 0 ≤ originalWidth
heq : 0 = originalWidth
⊢ { w := originalWidth, stream := (go aig inner).1.stream }.w = 0