(
    apply Or.intro_right
    apply Exists.intro ↑x
    apply And.intro
    (
        simp
        simp
        apply And.intro
        (
            apply Classical.byContradiction
            intros h₂
            simp at h₂
            apply h₁ h₂
            exact h₀
            exact h₀
        )
    )
)
case right.left
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ (∃ x_1 ∈ p.pcs, splitter &&& x_1 = ~~~splitter &&& ↑x) ∨ ∃ x_1 ∈ p.pcs, ~~~splitter &&& x_1 = ~~~splitter &&& ↑x

case right.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ c ∉ ⦃splitter⦄ ∧ c ∈ ⦃↑x⦄
no goals