Proof step 12 from proof rm-allsize (previous step)

a ∈ a ' + x0 ↔ a ∈ y, ∀ a0. a0 ∈ a ' + x0 ↔ a0 ∈ y, ∀ y. (∀ a. a ∈ x0 ↔ a ∈ y) → # rmdup(x0) = # rmdup(y) ⊦ 1 + # rmdup(x0) = # rmdup(y), a ∈ x0

Heuristic simplifier applied rule simplifier

Proof step 13:
a ∈ a ' + x0 ↔ a ∈ y, ∀ y. (∀ a. a ∈ x0 ↔ a ∈ y) → # rmdup(x0) = # rmdup(y), ∀ a0. a0 ∈ a ' + x0 ↔ a0 ∈ y ⊦ 1 + # rmdup(x0) = # rmdup(y), a ∈ x0