rcases i with ⟨b, (_|_)⟩
α : Type
i : α × Bool
c : List (α × Bool)
a : α
⊢ mem a (i :: c) ↔ a = i.fst ∨ mem a c
case mk.false
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, false) :: c) ↔ a = (b, false).fst ∨ mem a c

case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, true) :: c) ↔ a = (b, true).fst ∨ mem a c