intros c a h₀ b h₁ h₂ h₃
F : Type
p : ConfigPartition
pc : PC F
⊢ ∀ (c : Config F) (a : PC F),
    ((∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a) →
      ∀ (a_1 : PC F), ((∃ x ∈ p.pcs, pc &&& x = a_1) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a_1) → c ∈ ⦃a⦄ → c ∈ ⦃a_1⦄ → a = a_1
F : Type
p : ConfigPartition
pc : PC F
c : Config F
a : PC F
h₀ : (∃ x ∈ p.pcs, pc &&& x = a) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = a
b : PC F
h₁ : (∃ x ∈ p.pcs, pc &&& x = b) ∨ ∃ x ∈ p.pcs, ~~~pc &&& x = b
h₂ : c ∈ ⦃a⦄
h₃ : c ∈ ⦃b⦄
⊢ a = b