rw [go_denote_mem_prefix]
case inl
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
heq : curr = idx
⊢ ⟦{
        aig :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).aig,
        ref := (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref.cast ⋯ },
      assign.toAIGAssignment⟧ =
    (eval assign (var a)).getLsb curr
case inl
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
heq : curr = idx
⊢ ⟦{ aig := (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig,
        ref := { gate := ((aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref.cast ⋯).gate, hgate := ?inl.hstart } },
      assign.toAIGAssignment⟧ =
    (eval assign (var a)).getLsb curr

case inl.hstart
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
heq : curr = idx
⊢ ((aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref.cast ⋯).gate <
    (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig.decls.size