proposition: Theorem map_split_r : forall (A B C: Type)(ls : list (A * B))(f : B -> C), map f (snd (split ls)) = map (fun x => f (snd x)) ls.
proof: Proof. induction ls; intuition idtac; simpl in *. remember (split ls) as z. destruct z. simpl. f_equal. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation