# Exercise 3.5 List paramorphism operator: paraL ∷ (α → (List α, β) → β) → β → List α → β paraL f e Nil = e paraL f e (Cons x xs) = f x (xs, paraL f e xs) insert as a paraL instance: insertPara y = paraL f (wrap y) where f x (xs, ys) = if y < x then Cons y (Cons x xs) else Cons x ys We will prove that insert y xs = insertPara y xs for all finite lists xs by structural induction on xs. Case Nil: insertPara y Nil = { insertPara.1 } paraL f (wrap y) Nil = { paraL.1 } wrap y = { insert.1 } insert y Nil which establishes the case. Case Cons x xs: insertPara y (Cons x xs) = { insertPara.1 } paraL f (wrap y) (Cons x xs) = { paraL.2 } f x (xs, paraL f (wrap y) xs) = { insertPara, f.1 } if y < x then Cons y (Cons x xs) else Cons x (paraL f (wrap y) xs) Subcase y < x: = { subcase def., if } Cons y (Cons x xs) = { insert.2, subcase def. } insert y (Cons x xs) Subcase y ≥ x: = { subcase def., if } Cons x (paraL f (wrap y) xs) = { hypothesis } Cons x (insert y xs) = { insert.2, subcase def. } insert y (Cons x xs) which establishes the case. ∎