The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le dimanche 26 avril 2009 à 04:24 -0700, dimitrisg7 a écrit :

> Is it possible to get the nth object (of type rel (nth ...) (nth ...)) in
> the following inductive definition (I do not think that I can) or should I
> make some changes in my definitions?

You are missing a hypothesis on default values:

Variable rel_d : rel dA dB.

(or a hypothesis stating that n is bounded by the length of al).

Other than that, there should be no difficulty, it's just a
straightforward induction on n.

Proof.
induction n.
now intros al bl [|H].
intros al bl [|H].
easy.
intros.
now apply IHn.
Qed.

Best regards,

Guillaume