{
    intros h₄
    apply Exists.elim h₄
    intros x h₅
    simp [←h₅.right, semantics] at h₂
    apply Or.elim h₁
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        apply Not.elim h₂.left h₃.left
    }
    {
        intros h₆
        apply Exists.elim h₆
        intros y h₇
        simp[←h₇.right, semantics] at h₃
        have h₈ := p.disjoint c ⟨x, h₅.left⟩ ⟨y, h₇.left⟩ h₂.right h₃.right
        simp at h₈
        simp[←h₅.right, ←h₇.right, h₈]
    }
}
case right
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⦄
⊢ (∃ x ∈ p.pcs, ~~~pc &&& x = a) → a = b
no goals