rw [hasNegAssignment, addNegAssignment]
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ assignment.addNegAssignment.hasNegAssignment = true
case isFalse
assignment : Assignment
b : Bool
h✝ : ¬b = true
⊢ (match
      match assignment with
      | pos => both
      | neg => neg
      | both => both
      | unassigned => neg with
    | pos => false
    | neg => true
    | both => true
    | unassigned => false) =
    true