The Coq mailing list

[Jesper Louis Andersen <jesper.louis.andersen AT gmail.com>]

2011/11/20 Victor Porton 
<porton AT narod.ru>:
> So I fail to understand what eq_rect means. Could you explain?

The simplest solution is to ask Coq:

Coq < About eq_rect.
eq_rect :
forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y

Argument A is implicit
Argument scopes are [type_scope _ _ _ _ _]
eq_rect is transparent
Expands to: Constant Coq.Init.Logic.eq_rect

This tells you it is equivalent to eq_rect_r. There may be a reason
for having the alternative name, but I don't know it unfortunately. My
guess is the information can be found out by reading the source code.

Other likewise Vernacular commands are to be found here in the manual:
http://coq.inria.fr/doc/Reference-Manual009.html

Especially the Search-commands are useful. They allow you to hunt for
specific definitions and such in "reverse". You know there ought to be
a theorem X, but you only know its statement, not its name for
instance.

-- 
J.