rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩
case mp
α : Type
g : CNF α
h : ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
case mp.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : ∃ x, x ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)