dsimp at hgo
case signExtend
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 :
  (match go aig inner with
      | ⟨{ aig := eaig, stream := estream }, heaig⟩ =>
        let res := blastSignExtend eaig { w := originalWidth, stream := estream };
        ⟨res, ⋯⟩).val =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx
case signExtend
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
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign (signExtend v inner)).getLsb idx