subst this
case mk.isFalse
α : 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
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this✝ : idx = 0
this : 1 = newWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false