cases assignment <;> simp
assignment : Assignment
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => both
    | neg => neg
    | both => both
    | unassigned => neg) =
    both
no goals