formulas(goals).

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

end_of_list.
