∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} {assign : Std.Tactic.BVDecide.BVExpr.Assignment}
  (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (expr : Std.Tactic.BVDecide.BVExpr w) (refs : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    (∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign.toAIGAssignment, { aig := aig, ref := refs.get idx hidx }⟧ =
          (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx) →
      Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig (cache.insert expr refs)