Section foldl_List.
Require Export List.
Variable A:Set.
Variable B:Set.
Variable f:B->A->B.

Fixpoint foldl_list' (b:B)(l:list A){struct l}:B:=
match l with
nil => b
|cons a ls =>foldl_list' (f b a) ls
end.

End foldl_List.
Section foldl_Rose.
Require Export List.

Inductive Rose (A:Set):Set :=
 RCons: A -> list (Rose A) -> Rose A.
 
Variable A B:Set .
Variable eps:A->B->B.

Fixpoint foldl_Rose (b:B) (r:Rose A){struct r}:B:=
match r with
  RCons a rs => match rs with
      nil => eps a b
    | r::rs'=> (foldl_Rose  (foldl_list' (Rose A) B
                        (foldl_Rose) (eps a b) rs') r)
     end
end.
End foldl_Rose.  


Section CoeqRose.
Variable A B:Set.
Variable eps: A-> B -> B.
Implicit Arguments foldl_Rose.

Definition h1 :=fun (a:A) => fun (rs:list (Rose A))
    => fun (xs: B) => (RCons A a rs,eps a xs).
                      
Definition h2 :=fun (a:A) => fun (rs:list (Rose A))
    => match rs with
       nil => fun (xs:B) => (RCons A a nil,eps a xs)
     | cons  r rs' => match rs' with   
          nil => fun (xs: B) => (r , eps a (eps a xs))
        | r'::rs''=> fun (xs: B) => (r ,(foldl_list' (Rose A) B
                    (foldl_Rose A B eps) (eps a (eps a xs)) rs'))
                     end
       end.

Lemma ONE: forall rs:list (Rose A), forall a:A,forall xs:B,
((foldl_Rose  eps)   (snd (h1 a rs xs)) (fst (h1 a rs xs)) )=
 ((foldl_Rose  eps)  (snd (h2 a rs xs)) (fst (h2 a rs xs))).
 Proof.
 induction rs;intros.
 simpl.
 trivial.
 case rs.
 simpl.  
 auto.   
 intros;simpl.
 trivial.
 Defined.
End CoeqRose.                                      