The Coq mailing list

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

OK, "apply A with (Q := (y=3)) in H" also work. But result of this tactic
is confusing me. What seems unnatural for me is that in the same (second)
subgoal Coq once replaced Q by y = 2, and the other with y = 3:

H : x = 1 -> y = 2
============================
 (x = 1 -> y = 2) -> y = 3

Marko Malikoviæ

> You could have said as well "apply A with (Q := (y=3)) in H" and it
> would have worked, what shows that there is indeed no instance for Q
> that Coq could infer.
>
> Hope it helps.
>
> Hugo Herbelin
>

-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Arts and Sciences
University of Rijeka, Croatia
-----------------------------