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