Proof step 13 from proof last-elim (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 14:

  a = (a1 ' + x).last, a3 = a0, y1 = (a1 ' + x).butlast, ∀ a2, y0. a2 = (a1 ' + x).last ∧ y0 = (a1 ' + x).butlast ↔ a1 ' + x = y0 + a2 ' ⊦ a0 = a3 ∧ a1 ' + x = y1 + a '

• Proof step 16:

  a1 ' + x = y1 + a ', a0 = a3, ∀ a2, y0. a2 = (a1 ' + x).last ∧ y0 = (a1 ' + x).butlast ↔ a1 ' + x = y0 + a2 ' ⊦ a = (a1 ' + x).last ∧ a3 = a0 ∧ y1 = (a1 ' + x).butlast

Rule argument

Additional information