simp
case right.left.h.right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ~~~splitter &&& ↑x = ~~~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⦄
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⦄