rw [denote_go]
case isTrue.inr
α : 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
hlt : curr < idx
⊢ ⟦{
        aig :=
          (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).aig,
        ref :=
          (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).stream.getRef
            idx hidx1 },
      assign⟧ =
    ⟦f aig { lhs := lhs.getRef idx hidx1, rhs := rhs.getRef idx hidx1 }, assign⟧
case isTrue.inr
α : 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
hlt : curr < idx
⊢ ⟦f (f aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝ }).aig
        { lhs := (lhs.cast ⋯).getRef idx hidx1, rhs := (rhs.cast ⋯).getRef idx hidx1 },
      assign⟧ =
    ⟦f aig { lhs := lhs.getRef idx hidx1, rhs := rhs.getRef idx hidx1 }, assign⟧

case isTrue.inr.a
α : 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
hlt : curr < idx
⊢ curr + 1 ≤ idx