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