The Coq mailing list

[Karol Oslowski <ko181282 AT zodiac.mimuw.edu.pl>]

Hi,
   since about two weeks I'm completely stuck with prooving well 
foundness'ness of a relation R. I have the following definitions :
"
   Inductive seqFin : A -> Type :=
     | single: forall ( a : A ), seqFin a
     | cons: forall ( a b : A ) ( s : seqFin b ), R a b -> seqFin a.
 

   Definition seqInfAny := nat -> A.

   Definition seqInfOk2( seq : seqInfAny ) := forall n : nat, R ( seq n 
) ( seq ( S n ) ).

   Record seqInf : Type := make_seqInf{
     seqi : seqInfAny;
     seqOk : seqInfOk2 seqi
   }.

   Inductive seq : Type :=
     | finite : forall ( a : A ) ( s : seqFin a ), seq
     | infinite : forall ( s : seqInf ), seq.
"
I've prooven that :
"
  inductive A R /\ increasing A R -> (forall s : seq A R , isFinite s ).
"

And I want to proove the theorem:
"
inductive A R /\ increasing A R -> well_founded ( RInv R ).
"
I guess it should be very easy. I'm not giving the definitions of 
inductive and increasing because I guess they are not important.

I would be grateful for any sugestions.

kind regards

Karol Oslowski