Section Iteration.
Variable X:Set.   
Variable f:X -> X.  

Fixpoint iter (n:nat):X -> X:=
match n with
0 => fun x:X => x
 | (S n) => fun x:X => f (iter n x)
end.

Lemma Iter1:forall x:X, forall n:nat,iter n (f x)=f (iter n x).
Proof.
induction n;intros;simpl.
trivial.
rewrite IHn;trivial.
Defined.

End Iteration.

Section S.
Variable A B:Set.

Inductive S_A:Set :=
  L:A -> S_A
| I:S_A -> S_A.

Variable f:A -> B.
Variable g:B -> B.

Definition h1:=fun s:S_A=>fun b:B => (I s,b).
Definition h2:=fun s:S_A=>fun b:B => (s,g b).

Fixpoint foldl_S_A (b:B)(s:S_A){struct s}:B:=match s with
  L a => b
| I s'=> foldl_S_A (g b) s'
end.

(** % \newpage % *)

Lemma one: forall b:B, forall s:S_A,
(foldl_S_A (snd (h1 s b)) (fst (h1 s b)))=
                 (foldl_S_A (snd (h2 s b)) (fst (h2 s b))).
Proof.
intuition.
Defined.  

Fixpoint foldr_S_A (s:S_A){struct s}:B:=
match s with
   L a => f a  
 | I s => g (foldr_S_A s)
end.

Lemma ONE: forall a:A, forall n:nat,forall b:B, foldl_S_A b (iter S_A I n (L a))=
                 iter B g n b.
Proof.        
         induction n;intros;simpl.
           trivial.
           rewrite IHn.
           rewrite Iter1.
           intuition.
           Defined.             
Lemma TWO: forall a:A, forall n:nat, forall b:B, foldr_S_A (iter S_A I n (L a))=
                          iter B g n (f a).
Proof.
           induction n;intros;simpl.
           trivial.
           rewrite IHn;trivial.
           Defined.
Lemma THREE: forall a:A, forall n:nat,
foldl_S_A (f a) (iter S_A I n (L a)) =  foldr_S_A (iter S_A I n (L a)).                     
Proof.
                     intros.
                     rewrite ONE.
                     rewrite TWO;trivial.
                     exact (f a).
                     Defined.

                      
