rw [hasPosAssignment] at h
assignment : Assignment
h : ¬assignment.hasPosAssignment = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment
assignment : Assignment
h :
  ¬(match assignment with
      | pos => true
      | neg => false
      | both => true
      | unassigned => false) =
      true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => unassigned
    | neg => neg
    | both => neg
    | unassigned => unassigned) =
    assignment