data Nat = Zero | Succ Nat data List a = Nil | Cons a (List a) take (Succ n) (Cons x xs) = Cons x (take n xs) take (Succ n) Nil = Nil take Zero (Cons x xs) = Nil take n Nil = Nil twice f x = f (f x) ----------------------- twice (take n) = take n Equivalently (by function equality): twice (take n) xs = take n xs Proof by induction on structure of xs :: List a: Case xs = Nil: twice (take n) Nil = take n Nil take n (take n Nil) = take n Nil By cases on n :: Nat: Case n = Zero: take Zero (take Zero Nil) = take Zero Nil Nil = take Zero Nil Nil = Nil Case n = Succ m: take (Succ m) (take (Succ m) Nil) = take (Succ m) Nil Nil = take (Succ m) Nil Nil = Nil Case xs = Cons y ys; assume twice (take n) ys = take n ys twice (take n) (Cons y ys) = take n (Cons y ys) take n (take n (Cons y ys)) = take n (Cons y ys) By induction on n :: Nat: Case n = Zero: take Zero (take Zero (Cons y ys)) = take Zero (Cons y ys) Nil = take Zero (Cons y ys) Nil = Nil Case n = Succ m; assume take m (take m (Cons y ys)) = take m (Cons y ys) ________________________________________________ take (Succ m) (take (Succ m) (Cons y ys)) = take (Succ m) (Cons y ys) take (Succ m) (Cons y (take m ys)) = take (Succ m) (Cons y ys) Cons y (take m (take m ys)) = take (Succ m) (Cons y ys) Cons y (take m (take m ys)) = Cons y (take m ys) take m (take m ys) = take m ys