rintro (⟨c, mx, mc⟩ | ⟨c, my, mc⟩)
case mpr
α : Type
a : α
x y : CNF α
⊢ ((∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c) → ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c
case mpr.inl.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
mx : c ∈ x
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c

case mpr.inr.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
my : c ∈ y
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c