. have : idx = 0 := by omega
  simp only [this]
  have : 1 = newWidth := by omega
  subst this
  rw [← hextract]
  split
  . rw [RefStream.getRef_in_bound]
    dsimp
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . congr 2
    . omega
  . rw [RefStream.getRef_out_bound]
    . simp
    . omega
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
⊢ ⟦{ 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
no goals