cases assignment <;> simp
case isTrue
assignment : Assignment
b : Bool
h✝ : b = true
⊢ (match
      match assignment with
      | pos => pos
      | neg => both
      | both => both
      | unassigned => pos with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    true
no goals