proposition: Theorem fst_split_perm : forall (A B : Type)(ls1 ls2 : list (A * B)), Permutation ls1 ls2 -> Permutation (fst (split ls1)) (fst (split ls2)).
proof: Proof. induction 1; intuition idtac; simpl in *. econstructor. remember (split l) as z. destruct z. remember (split l') as z. destruct z. simpl. econstructor. eauto. remember (split l) as z. destruct z. simpl. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation