∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignment = true ↔
    Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
        (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment (decide ¬b = true) assignment) =
      true