proposition: Theorem fst_split_cons : forall (A B : Type)(ls : list (A * B)) p, fst (split (p :: ls)) = (fst p) :: (fst (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