[SOLVED] What does ==> mean in proverif?

What does ==> mean in proverif?

I found the following line of code in the proverif manual.

 ⋮ 
query event(evCocks) ==> event(evRSA).
 ⋮

What does ==> mean?

EDIT: I have answered my own question below.

Solution

Correspondence properties:
  P and Q are predicates.

    P(x) ==> Q(x, y)

      for all x where P(x) is true, then there exists a y 
      such that Q(x, y) is true

query event(e1) ==> event(e2).

  the query above can be translated to the following question:
    Is it true that;
         for all executions of event e1 (in the protocol) it is true that 
         e2 has executed?

In the proverif manual it is stated that

query event(evCocks) ==> event(evRSA)

is true if and only if, for all executions of the protocol, if the event 
evCocks has been executed, then
event evRSA has also [already] been executed

link to proverif manual