The Coq mailing list

[casteran AT labri.fr]

Hello,

 I have some difficulties ine adapting the proof of unicity
of proofs of n <= m (Coq, Faq, question 136).


 At some moment, we've got the following goal :

  n : nat
  q : n <= n
  ============================
   forall e : n = n, eq_rect n (fun n0 : nat => n <= n0) (le_n n) n e
                     = q


 The sequence (which works :-)) is :

  pattern n at 2 4 6 10, q; case q; [intro | intros m l e].

  If I count the occurrences of "n" in the subgoal above, I find only
 6 of them (8 if I count the type of le_n n), but not 10.

 Is there a way to infer which argument is to be given to pattern from
the current goal?


 More generally, where can I find some more examples of proofs of
 proof unicity?

Thanks in advance,

Pierre










----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.