proposition: Theorem snd_split_cons : forall (A B : Type)(ls : list (A * B)) p, snd (split (p :: ls)) = (snd p) :: (snd (split ls)).
proof: Proof. intuition idtac; simpl in *. remember (split ls) as z. destruct z. simpl. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation