Proof step 8 from proof size-del-nodups (previous step)

a ∈ x0, ∀ m0, a1. # x0 = m0 + 1 ∧ a1 ∈ x0 → #(x0 -l a1) = m0 ∨ x0 = [] ⊦ 1 + #(x0 -l a) = # x0, x0 = [], dups(x0), a0 ∈ x0

Heuristic simplifier applied rule simplifier

Proof step 9:
a ∈ x0, ∀ m, a1. # x0 = m + 1 ∧ a1 ∈ x0 → #(x0 -l a1) = m ⊦ 1 + #(x0 -l a) = # x0, x0 = [], dups(x0), a0 ∈ x0