The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Thanks,

I understand Florian's explanation but I still think it is little strange
- syntax "rewrite ident1 in ident2" has nothing to do with any goal or
subgoals. It must to work only with ident1 and ident2 from context.
But furthermore, my sample from last e-mail is not my real situation. I
have stranger situation. Before assumption, I have "exists x" and not
"split". So, solution:

split; [assumption | rewrite For_rewriting in H]

does not work in my case.

Furthermore, Thery's solution:

split; (try assumption); rewrite ...

is not good because my combination must to fail if assumption fail.
Thery's solution never fails.

I think I must redefine everything because I have situation like this:

first[exists x1;exists y1;assumption;rewrite Hypothesis_1 in Hypothesis_2|
...
|exists xn;exists yn;assumption;rewrite Hypothesis_n in Hypothesis_m]

Thank you very much,

Marko Malikoviæ