. intro h
  rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩
  rcases hclause2 with ⟨lit, hlit⟩
  exists lit.fst, clause
  constructor
  . assumption
  . rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
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
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x