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