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

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

Heuristic simplifier applied rule simplifier

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