proposition: Theorem list_pred_fst_split_flatten_eq_l : forall (A B : Set)(a : list (list (A * B)))(b : list (list A)), list_pred (list_pred (fun a0 b0 => fst a0 = b0)) a b -> flatten b = fst (split (flatten a)).
proof: Proof. induction a; intuition; simpl in *. inversion H; clear H; subst. trivial. inversion H; clear H; subst. simpl. rewrite fst_split_app_eq. f_equal. eapply list_pred_fst_split_eq_l . trivial. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation