constructor
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
case mp
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) → ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

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