Lemma: mapTree (f . g) t .=. mapTree f (mapTree g t) Proof by induction on Tree t Case Empty To show: mapTree (f . g) Empty .=. mapTree f (mapTree g Empty) Proof mapTree (f . g) Empty (by def mapTree) .=. Empty mapTree f (mapTree g Empty) (by def mapTree) .=. mapTree f Empty (by def mapTree) .=. Empty QED Case Node x t1 t2 To show: mapTree (f . g) (Node x t1 t2) .=. mapTree f (mapTree g (Node x t1 t2)) IH1: mapTree (f . g) t1 .=. mapTree f (mapTree g t1) IH2: mapTree (f . g) t2 .=. mapTree f (mapTree g t2) Proof mapTree (f . g) (Node x t1 t2) (by def mapTree) .=. Node ((f.g) x) (mapTree (f.g) t1) (mapTree (f.g) t2) (by def .) .=. Node (f(g x)) (mapTree (f.g) t1) (mapTree (f.g) t2) (by IH1) .=. Node (f(g x)) (mapTree f (mapTree g t1)) (mapTree (f.g) t2) (by IH2) .=. Node (f(g x)) (mapTree f (mapTree g t1)) (mapTree f (mapTree g t2)) mapTree f (mapTree g (Node x t1 t2)) (by def mapTree) .=. mapTree f (Node (g x) (mapTree g t1) (mapTree g t2)) (by def mapTree) .=. Node (f(g x)) (mapTree f (mapTree g t1)) (mapTree f (mapTree g t2)) QED QED