Theorem: CNF.mem_cons (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α : Type
a : α
i : Clause α
c : CNF α
⊢ mem a (i :: c) ↔ Clause.mem a i ∨ mem a c
Tactic:
simp [mem]
State after:
no goals