I've found a solution to my problem. Instead of directly using the proof
stack, I proved some rules and wrote helper functions, and the helper
functions generate proofs for a number of small theorems (corresponding
to the subgoals in my original post). I compose my big theorem from the
small th
Hi,
I have a situation where I don't know what the best solution is.
I have a goal of the form x ==> y, and after an initial rewrite on x and
after REPEAT STRIP_TAC, I have a list of subgoals. Here's the problem.
1) According to different situations, the length of the list of subgoals
varies;
