formulas(goals).

   (Period(x,u) & Period(y,u) & -Shorter(u,x * y))
      -> (exists u3 (u = x * u3)) # label("Lemma Reform-2a").

end_of_list.

formulas(assumptions).

  % general lemma (proved)

   (u * u1 = x * x1 & -Shorter(u,x * y)) -> (exists u3 (u = x * u3))
      # label("Lemma 4").

end_of_list.
