formulas(goals).

   Prefix(x,y) -> Shorter(x,y) # label("Lemma 2").

end_of_list.

