Hi Waqar,
Firstly (simplest),
SPLIT_LT 2 (ALLGOALS tac1, ALL_LT)
applies tac1 to the first two subgoals and does nothing to the
remainder. Then you can work on the remaining goal.
But you want to also apply EVERY [tac2, tac3, ...] to the third subgoal
(which is the only remaining one),
Hi,
Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply
tac1 and the third goal may takes some set of tacts, say tac2, tac3...
Is it possible that I can use SPLIT_LT in a way such that first two
subgoals are discharged by applying tac1 and I only end up proving the
third
