RelevantGoals

The goals selected so far in a frame, the newest first: a chain extended at each step, rather than the set of their variables (arg2p: copying the set at each step made long conjunctions quadratic). The variables are only collected when a substitution is trimmed.