rcases target with ⟨input, hi, lo, hnew⟩
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hextract : blastExtract aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
    else false
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : (ExtractTarget.mk input hi lo hnew).lo + idx < (ExtractTarget.mk input hi lo hnew).w then
      ⟦{ aig := aig,
          ref := (ExtractTarget.mk input hi lo hnew).stream.getRef ((ExtractTarget.mk input hi lo hnew).lo + idx) h },
        assign⟧
    else false