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

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