Proof step 2 from proof eq-01 (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  [] + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0 ⊦ b = c, a = b, a = c, a ∈ y, a ∈ [], a ∈ z, c ∈ [], c ∈ z, dups([] + z)

• Proof step 11:

  ∀ a, b, y, c, z, x0, z0. x1 + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0 → b = c ∨ a = b ∨ a = c ∨ a ∈ y ∨ a ∈ x1 ∨ a ∈ z ∨ c ∈ x1 ∨ c ∈ z ∨ dups(x1 + z), (a0 + x1) + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0 ⊦ b = c, a = b, a = c, a ∈ y, a ∈ a0 + x1, a ∈ z, c ∈ a0 + x1, c ∈ z, dups((a0 + x1) + z)

Rule argument

Additional information

Used simplifier rules: list freely generated by [], +;;