--- a/systemF.agda	Fri Apr 18 14:03:54 2014 +0900
+++ b/systemF.agda	Tue Apr 22 11:11:50 2014 +0900
@@ -191,4 +191,25 @@
 lemma-binary-tree-it-leaf = refl
 
 lemma-binary-tree-it-tree : {l : Level} {W : Set l} {w : W} {f : W -> W -> W} {u v : BinTree} -> BinTreeIt w f (couple u v)  ≡ f (BinTreeIt w f u) (BinTreeIt w f v)
-lemma-binary-tree-it-tree = refl
\ No newline at end of file
+lemma-binary-tree-it-tree = refl
+
+
+-- Tree
+
+Tree : {l : Level} -> (U : Set l) -> Set (suc l)
+Tree {l} U = {X : Set l} -> X -> ((U -> X) -> X) -> X
+
+Leaf : {l : Level} {U : Set l} -> Tree U
+Leaf {l} {U} = \{X : Set l} -> \(x : X) -> \(y : (U -> X) -> X) -> x
+
+collect : {l : Level} {U : Set l} -> (U -> Tree U) -> Tree U
+collect {l} {U} f = \{X : Set l} -> \(x : X) -> \(y  : ((U -> X) -> X)) -> y (\(z : U) -> f z {X} x y)
+
+TreeIt : {l : Level} {U W : Set l} -> W -> ((U -> W) -> W) -> Tree U -> W
+TreeIt {l} {U} {W} w h t = t {W} w h
+
+lemma-tree-it-nil : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} -> TreeIt {l} {U} {W} w h Leaf ≡ w
+lemma-tree-it-nil = refl
+
+lemma-tree-it-collect : {l : Level} {U W : Set l} {w : W} {h : (U -> W) -> W} {f : U -> Tree U} -> (TreeIt w h (collect f)) ≡ (h (\(x : U) -> TreeIt w h (f x)))
+lemma-tree-it-collect = refl