The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Hello,

let me add a word on Solange's answer. Note that Eqdep introduces an
axiom, namely

Axiom eq_rec_eq :
  (U:Set; p:U; Q:(U->Set); x:(Q p); h:(p=p))x=(eq_rec U p Q x p h).

You can prove your result without any axiom, because equality on nat is
decidable. Eqdep_dec proves a few lemmas about this. Here is a proof:

Require Eqdep_dec.
Require Peano_dec.
Lemma test: (v:(natvect O))v=empty.
Intros v.
Change v=(eq_rec ? ? natvect empty ? (refl_equal ? O)) .
Generalize (refl_equal ? O).
Change ([n:nat; v:(natvect n)](e:(O=n))v=(eq_rec ? ? natvect empty ? e)
O v) .
Case v; Intros.
Apply K_dec_set with p:=e.
Exact eq_nat_dec.

Reflexivity.

Discriminate e.
Save.


Best regards,

Bruno Barras.

-- 
  Projet LogiCal - INRIA Rocquencourt
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://logical.inria.fr/~barras
-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/