cases Nat.eq_or_lt_of_le hidx2 with
| inl heq =>
  rw [← hgo]
  rw [go_getRef]
  rw [AIG.RefStream.getRef_push_ref_eq']
  . simp only [← heq]
    rw [go_denote_mem_prefix]
    . simp
    . simp [Ref.hgate]
  . rw [heq]
| inr hlt =>
  rw [← hgo]
  rw [denote_go]
  . simp [getRef_cast, -Ref_cast']
  . omega
case isTrue
α : Type
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : DecidableEq α
aig✝ : AIG α
len : Nat
assign : α → Bool
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefStream curr
input : aig.RefStream len
f : (aig : AIG α) → aig.Ref → Entrypoint α
inst✝¹ : LawfulOperator α Ref f
inst✝ : LawfulMapOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig (input.getRef curr h✝)).aig (curr + 1) ⋯ ((s.cast ⋯).pushRef (f aig (input.getRef curr h✝)).ref)
      (input.cast ⋯) f =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ = ⟦f aig (input.getRef idx hidx1), assign⟧
no goals