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