Proof step 6 from proof dups-appex (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  a ∈ y, dups(x0 + y) ↔ (∃ a. a ∈ x0 ∧ a ∈ y), ∀ y0. dups(x0 + y0) ↔ dups(y0) ∨ (∃ a. a ∈ x0 ∧ a ∈ y0) ⊦ dups(x0), dups(y), a ∈ x0, ∃ a0. (a0 = a ∨ a0 ∈ x0) ∧ a0 ∈ y

• Proof step 8:

  dups(x0 + y), dups(x0 + y) ↔ (∃ a. a ∈ x0 ∧ a ∈ y), ∀ y0. dups(x0 + y0) ↔ dups(y0) ∨ (∃ a. a ∈ x0 ∧ a ∈ y0) ⊦ dups(x0), dups(y), a ∈ x0, ∃ a0. (a0 = a ∨ a0 ∈ x0) ∧ a0 ∈ y

Rule argument

Additional information