unfold blastExtract at hextract
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 : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (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 :
  (match ExtractTarget.mk input hi lo hnew with
    | ExtractTarget.mk input hi lo hnew =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      if h : lo ≤ hi then { aig := aig_1, stream := blastExtract.go input lo 0 ⋯ falseRef RefStream.empty }
      else
        let_fun this := ⋯;
        let base := RefStream.empty;
        let base := base.pushRef (input.getRefD lo falseRef);
        { aig := aig_1, stream := this ▸ base }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false