Set: pp::colors
  Set: pp::unicode
  Imported 'tactic'
  Defined: xor
⊤ ⊕ ⊥
  Assumed: a
a ⊕ a ⊕ a
@subst : ∀ (A : (Type U)) (a b : A) (P : A → Bool), P a → a = b → P b
  Proved: EM2
EM2 : ∀ a : Bool, a ∨ ¬ a
EM2 a : a ∨ ¬ a
  Proved: xor_neq