intros
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign expr).getLsb idx
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (bitblast aig expr).aig, ref := (bitblast aig expr).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx✝