Theorem: Assignment.not_hasNeg_of_removeNeg (LeanSAT/LRAT/Assignment.lean)

State before:
assignment : Assignment
⊢ ¬assignment.removeNegAssignment.hasNegAssignment = true
Tactic:
simp only [removeNegAssignment, hasNegAssignment, Bool.not_eq_true]
State after:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => unassigned
      | both => pos
      | unassigned => unassigned with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false

State before:
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => unassigned
      | both => pos
      | unassigned => unassigned with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    false
Tactic:
cases assignment <;> simp
State after:
no goals