simp[semantics] at h₁
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∉ ⦃splitter &&& ↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄
case right
F : Type
p : ConfigPartition
splitter : PC F
c : Config F
x : ↑p.pcs
h₀ : c ∈ ⦃↑x⦄
h₁ : c ∈ ⦃splitter⦄ → c ∉ ⦃↑x⦄
⊢ ∃ a, ((∃ x ∈ p.pcs, splitter &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~splitter &&& x = a) ∧ c ∈ ⦃a⦄