The Coq mailing list

[anabelcesar <anabelcesar AT gmail.com>]

Dear Coq users,

I am working with families of sets F:nat -> Set and I need to 
extend them using a particular set as the first set of the family.
In the example below, I use "unit". 

Then, If we iterate the construction n times, the n first sets should be unit
(and in particular the set n in the family). But I do not know how to prove this
(probably easy) Lemma.

Any help is appreciated.

Cesar


-----------------------------------------------------------------  
Section Function_extension.

Variable F:nat-> Set.


Definition unit_ext: nat -> Set:=
fun n : nat => match n with
               | 0 => unit
               | S n0 => F n0
               end.
End Function_extension.

Fixpoint iterated_unit_ext ( F:nat-> Set)(n:nat){struct n}:=
 match n with
               | 0 => unit_ext F
               | S n => iterated_unit_ext (unit_ext F) n
               end.

Lemma aa:forall (n:nat) (F:nat -> Set), iterated_unit_ext  F  n n  = unit.
Proof.

------------------------------------------------------------------