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

State before:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ mem a g
Tactic:
apply Exists.intro c
State after:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ c ∈ g ∧ Clause.mem a c

State before:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ c ∈ g ∧ Clause.mem a c
Tactic:
constructor <;> assumption
State after:
no goals