The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Hi,

I am new here, trying to lean the basics of Coq, and have already successfully
proved a few very simple theorems. However, I can´t manage to find a solution
for the first part of exercise 5.9 of "Interactive Theorem Proving..." (page
124). The solution shows the use of:

intros x [H1 | H1]

Although I understand "intros x" and the other tactics used in the solution, I
have no idea what the meaning of the [H1 | H1] next to it is. I have tried to
find it in the documentation, however without success. Can anyone explain this
to me?

Thanks in advance,
Marcus.