Proof step 24 from proof diff-sub-size (previous step)

# s0 = n0 + # s ∧ # s ≤ # s0, #(s0 \ s) = n0, a ∈ s0, a0 ∈ s0, ∀ a0. a0 ∈ s ++ a → a0 ∈ s0 ⊦ n0 - 1 = # s0 - # s + 1, a ∈ s

Heuristic simplifier applied rule simplifier

Proof step 25:
# s0 = #(s0 \ s) + # s, # s ≤ # s0, a ∈ s0, a0 ∈ s0, ∀ a0. a0 ∈ s ++ a → a0 ∈ s0 ⊦ #(s0 \ s) - 1 = # s0 - # s + 1, a ∈ s