split at lacks_pos <;> simp_all (config := { decide := true })
assignment : Assignment
lacks_neg : ¬assignment.hasNegAssignment = true
lacks_pos :
  (match assignment with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ assignment = unassigned
no goals