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

User applied rule case distinction

And obtained the following new goals

• Proof step 32:

  a0 ∈ x0, rmdup(z) = y + a ' + z0, a ∈ z, a0 ≠ a → (a0 ∈ x0 ↔ a0 ∈ y0 ∨ a0 ∈ z) ⊦ a0 ∈ y0 ∨ a0 ∈ y ∨ a0 ∈ z0, # rmdup(x0) = # rmdup((y0 + y) + z0), a ∈ y0, a ∈ x0, a ∈ y, a ∈ z0

• Proof step 36:

  a0 ∈ y0 ∨ a0 ∈ y ∨ a0 ∈ z0, rmdup(z) = y + a ' + z0, a ∈ z, a0 ≠ a → (a0 ∈ x0 ↔ a0 ∈ y0 ∨ a0 ∈ z) ⊦ a0 ∈ x0, # rmdup(x0) = # rmdup((y0 + y) + z0), a ∈ y0, a ∈ x0, a ∈ y, a ∈ z0

Rule argument

Additional information