The Coq mailing list

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

Dear all,

assume that we have context:

H : _
H0 : _
H1 : _
...
Hn : _
-----------------
Goal

and an axiom A.

I'm searching for a simply way to apply axiom A in all hypotheses H, H0,
H1, ... , Hn at once.

Is there some simply way to do that?

Thank you very much,

Marko Malikoviæ

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