exists lit.fst, clause
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g ∧ ((lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause)