(
    intro h₁
    simp[semantics] at h₁
    apply Exists.intro (~~~splitter &&& x)
    simp[semantics]
    apply And.intro
    (
        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
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
⊢ c ∉ ⦃splitter &&& ↑x⦄ → ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
no goals