∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (result : aig.ExtendingEntrypoint)
  (cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig) (result_1 : aig.ExtendingEntrypoint)
  (cache_1 : Std.Tactic.BVDecide.BVExpr.Cache (↑result_1).aig),
  ({ result := result, cache := cache } = { result := result_1, cache := cache_1 }) =
    (result = result_1 ∧ cache ≍ cache_1)