introduce list_tactic - works on a list of goals, not a single goal
define op THEN_LT (tac1, ltac2 : list_tactic).
A tactical that applies ltac2 to the list of subgoals resulting from tac1;
TACS_TO_LT (tac2l: tactic list) : list_tactic
REVERSE_LT: A list_tactic that reverses a list of subgoals