intro h
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
case mpr
α : Type
g : CNF α
h : ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
⊢ ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x