rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
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 := (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).aig,
        ref :=
          (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (BitVec.signExtend v (eval assign inner)).getLsb idx
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 := (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).aig,
        ref :=
          (blastZeroExtend (go aig inner).1.aig { w := originalWidth, stream := (go aig inner).1.stream }).stream.getRef
            idx hidx },
      assign.toAIGAssignment⟧ =
    (BitVec.zeroExtend v (eval assign inner)).getLsb idx

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
⊢ (eval assign inner).msb = false