
Section foldl_Tree.
Variable A:Set.
Variable B:Set.
Variable f:A -> B.
Variable g:B -> B -> B.

Definition k:=fun a:A=>fun b:B=>g (f a) b.

Inductive Tree (A:Set):Set :=
   Leaf:A -> Tree A
 | Bin:Tree A -> Tree A -> Tree A.
 
Fixpoint foldl_Naish (b:B)(l:Tree A){struct l}:B:=
match l with
   Leaf a => (k a b)
 | Bin l r => foldl_Naish (foldl_Naish (g b b) l) r
end.

Definition h1 := fun (l r:Tree A) => fun (b1 b2:B) => (Bin A l r,g b1 b2 ).
Definition h2 := fun (l r:Tree A) => fun (b1 b2:B) =>
                                  (r,foldl_Naish   (g (g b1 b2) (g b1 b2)) l) .
                                  
Lemma one: forall a:A, forall b1 b2:B, forall lt1 lt2:Tree A,
(foldl_Naish
      (snd (h1 lt1 lt2 b1 b2)) (fst (h1 lt1 lt2 b1 b2)))=
(foldl_Naish  (snd (h2 lt1 lt2 b1 b2)) (fst (h2 lt1 lt2 b1 b2)) ).
            Proof.
            intros.
            simpl. 
            auto.  
            Qed.   
End foldl_Tree.
            
            