proposition: Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X), map f (rev l) = rev (map f l).
proof: Proof. Admitted. Fixpoint flat_map {X Y: Type} (f: X -> list Y) (l: list X) : list Y . Admitted. Example test_flat_map1: flat_map (fun n => [n;n;n]) [1;5;4] = [1; 1; 1; 5; 5; 5; 4; 4; 4]. Admitted. Definition option_map {X Y : Type} (f : X -> Y) (xo : option X) : option Y := match xo with | None => None | Some x => Some (f x) end. Fixpoint fold {X Y: Type} (f : X->Y->Y) (l : list X) (b : Y) : Y := match l with | nil => b | h :: t => f h (fold f t b) end. Check (fold andb) : list bool -> bool -> bool. Example fold_example1 : fold mult [1;2;3;4] 1 = 24. Proof. reflexivity. Qed.