. intro h
  rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩
  exists clause
  constructor
  . assumption
  . cases hclause2 with
    | inl hl => exact Exists.intro _ hl
    | inr hr => exact Exists.intro _ hr
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
no goals