The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 04/07/2013 03:12 PM, AUGER Cédric wrote:
> That is cheating, you are using an axiom ^^
>
> Print eq_dep_eq_dec.
> Print eq_rect_eq__eq_dep_eq.
> Print eq_rect_eq.
> Print Eq_rect_eq.eq_rect_eq.
Since my previous reply was kind of short, let me show where your 
analysis fails.

Print eq_rect_eq__eq_dep_eq.

gives

  eq_rect_eq__eq_dep_eq =
  λ (U : Type) (eq_rect_eq : Eq_rect_eq U) (P : U → Type)
    (p : U) (x y : P p) (H : eq_dep U P p x p y),
    eq_rect_eq__eq_dep1_eq U eq_rect_eq P p x y
      (eq_dep_dep1 U P p p x y H)
     : ∀ U : Type, Eq_rect_eq U → Eq_dep_eq U

we see that eq_rect_eq is the name of an argument of 
eq_rect_eq__eq_dep_eq, and it is not eq_rect_eq itself, which indeed 
uses an axiom.