unfold blastSignExtend at hg
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg : blastSignExtend aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
htarget : 0 < target.w
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hg :
  (match target with
    | { w := width, stream := input } =>
      if hw : width = 0 then blastZeroExtend aig { w := width, stream := input }
      else { aig := aig, stream := blastSignExtend.go width ⋯ input newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if hidx : idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef idx hidx }, assign⟧
    else ⟦{ aig := aig, ref := target.stream.getRef (target.w - 1) ⋯ }, assign⟧