formulas(goals).

   (x * y = u * v) -> ( Prefix(x,u) | Prefix(u,x) | x = u ) # label("Lemma 1").

end_of_list.

