The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 04/07/2013 03:12 PM, AUGER Cédric wrote:
> > Require Import Eqdep Eqdep_dec Omega Utf8.
> >
> > Lemma nat_le_pi: ∀ (x y : nat) (p q : x<  y), p = q.
> > Proof.
> >     assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
> >       y = y' → eq_dep nat (le x) y p y' q) as aux.
> >     { fix 3. intros x ? [|y p] ? [|y' q].
> >       * easy.
> >       * clear nat_le_pi. omega.
> >       * clear nat_le_pi. omega.
> >       * injection 1. intros Hy. now case (nat_le_pi x y p y' q Hy). }
> >     intros x y p q. now apply (eq_dep_eq_dec eq_nat_dec), aux.
> > Qed.
>
> That is cheating, you are using an axiom ^^

Not according to Coq: [Print Assumptions nat_le_pi.] gives:

Warning: query commands should not be inserted in scripts
Closed under the global context