cases b
α✝ : Type
a : α✝
b : Bool
c : Clause α✝
h : (a, b) ∈ c
⊢ mem a c
case false
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ mem a c

case true
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ mem a c