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 [-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
lhs rhs : aig.RefStream len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx1 : idx < len
hidx2 : curr ≤ idx
res : RefStreamEntry α len
h✝ : curr < len
hgo :
  go (f aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝ }).aig (curr + 1)
      ((s.cast ⋯).pushRef (f aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝ }).ref) ⋯ (lhs.cast ⋯)
      (rhs.cast ⋯) f =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign⟧ =
    ⟦f aig { lhs := lhs.getRef idx hidx1, rhs := rhs.getRef idx hidx1 }, assign⟧
no goals