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
p : Bool → Prop
x✝ : ∃ b, p b
b : Bool
h : p b
⊢ p false ∨ p true
cases b
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
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
exact Or.inl h
no goals
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
exact Or.inr h