Best practice would probably be to write
`!n. n = C’ == n w` by METIS_TAC[]
You can also look at things like Q.SUBGOAL_THEN
Michael
On 13 May 2014, at 6:01 pm, masoume tajvidi mas.tajv...@gmail.com wrote:
Hi ,
I have a subgoal like this:
F
I suspect lcsymtacs.rfs[] (aka REV_FULL_SIMP_TAC (srw_ss()) []) will do it
in your particular example.
Alternatively, you could use REPEAT BasicProvers.VAR_EQ_TAC THEN
FULL_SIMP_TAC std_ss [].
These will all change your goal state in more ways than one.
On Tue, May 13, 2014 at 9:01 AM, masoume
Hi Masoume,
Have you tried RES_TAC? I think RES_TAC should get you ∀n. n ≤ C' ⇒ n
≠ w as an assumption.
Cheers,
Magnus
On 13 May 2014 09:01, masoume tajvidi mas.tajv...@gmail.com wrote:
Hi ,
I have a subgoal like this:
F
0. (winner' =
Thank you all for your quick response.
Actually all these Tactics work but they are so smart that disappear what I
want to stay there in the assumptions( ∀n. n ≤ C' ⇒ n ≠ w).
I assume I need a very basic Tactic for exactly this aim and no more
simplification.
Cheers,
Masoumeh
On Tue, May 13,
