Theorem: Misc.Bool.exists_bool (LeanSAT/Util/Misc.lean)

State before:
p : Bool → Prop
x✝ : ∃ b, p b
b : Bool
h : p b
⊢ p false ∨ p true
Tactic:
cases b
State after:
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true

case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true

State before:
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true

case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Tactic:
exact Or.inl h
State after:
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true

State before:
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
Tactic:
exact Or.inr h
State after:
no goals