. rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause
no goals