omega
α : 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 :
  (if hw : target.w = 0 then blastZeroExtend aig { w := target.w, stream := target.stream }
    else { aig := aig, stream := blastSignExtend.go target.w ⋯ target.stream newWidth 0 ⋯ RefStream.empty }) =
    res
⊢ ¬target.w = 0
no goals