The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Tue, 15 May 2007 15:48:46 +0100,
Edsko de Vries 
<devriese AT cs.tcd.ie>
 a écrit :

> What I don't know is (a) if there can be infinite proofs of typeof,
> even though typeof is inductive,

Yes a term of an inductive type typeof is necessarily finite.

> and (b) if there cannot, how I can
> express that after having applied T_Exchange a number of times,
> another rule must have been applied. 

The argument you should use is something like "if there are two
consecutive applications of the swapping rule, then there is a single
equivalent one". Once you have proved this, then you can use
contradiction by saying that after one application of swapping rule
if there is a proof of typeof t T then there is one which does not
start with a swap.

Best regards,
Pierre Courtieu