Hello, I'm trying to prove the unfold fusion law, as given in the chapter "Origami Programming" in "The Fun of Programming". unfold is defined like this: unfold p f g b = if p b then [] else (f b):unfold p f g (g b) And the law states: unfold p f g . h = unfold p' f' g' with p' = p.h f' = f.h h.g' = g.h Foremost I don't really see why one would want to fuse h into the unfold. h is executed once, at the beginning and is never needed again. Can someone give me an example? So, this is what I got so far: unfold p f g.h = (\b -> if p b then [] else (f b): unfold p f g (g b).h = if p (h b) then [] else (f (h b)) : unfold p f g (g (h b)) = if p' b then [] else f' b: unfold p f g (h (g' b)) not very much. I kinda see why it works after I "unfold" some more, but I can't really prove it. I suspect I need some technique I haven't learned yet. I've heard about fixpoint induction, that looks promising, but Google knows very little about it. I hope somebody can give me some hints. Regards, Adrian