For example, the command
causes LP to generate a single subgoal which involves proving the formulaprove when \A x:Elem (x \in s:Set <=> x \in t:Set) yield s = t
\A x:Elem (x \in s:Set <=> x \in t:Set) => s = t
LP also generates a single subgoal when asked to initiate a proof of a partitioned-by. This subgoal is the one associated with the translation of the partitioned-by into a deduction rule.