proposition: Theorem list_pred_fst_split_eq : forall (A B C : Set)(ls1 : list (A * B))(ls2 : list (A * C)), list_pred (fun a b => fst a = fst b) ls1 ls2 -> fst (split ls1) = fst (split ls2).
proof: Proof. induction 1; intuition; simpl in *. destruct a1. destruct a2. remember (split ls1) as z. destruct z. remember (split ls2) as z. destruct z. simpl in *. subst. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation