cases a1 with
  | true =>
      cases a2 with
      | true => rfl
      | false => nomatch h
  | false =>
        cases a2 with
        | true => nomatch h
        | false => rfl
a1 a2 : Bool
h : Bool.not a1 = Bool.not a2
⊢ a1 = a2
no goals