intro idx hidx1 hidx2
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx1 : idx < w),
    curr ≤ idx →
      ⟦{ aig := (go w aig curr s a hcurr).aig, ref := (go w aig curr s a hcurr).stream.getRef idx hidx1 },
          assign.toAIGAssignment⟧ =
        (eval assign (var a)).getLsb idx
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
⊢ ⟦{ aig := (go w aig curr s a hcurr).aig, ref := (go w aig curr s a hcurr).stream.getRef idx hidx1 },
      assign.toAIGAssignment⟧ =
    (eval assign (var a)).getLsb idx