α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : Prop
⊢ x = True ∨ x = False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : Prop
⊢ x ∈ {True, False}
rw [mem_insert_iff, mem_singleton_iff]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : Prop
⊢ x = True ∨ x = False
exact Classical.propComplete x