simp[←h₇.right, semantics] at h₃
case right.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 ∈ ⦃b⦄
h₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
⊢ a = b
case right.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₄ : ∃ x ∈ p.pcs, ~~~pc &&& x = a
x : PC F
h₅ : x ∈ p.pcs ∧ ~~~pc &&& x = a
h₂ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃x⦄
h₆ : ∃ x ∈ p.pcs, ~~~pc &&& x = b
y : PC F
h₇ : y ∈ p.pcs ∧ ~~~pc &&& y = b
h₃ : c ∉ ⦃pc⦄ ∧ c ∈ ⦃y⦄
⊢ a = b