proposition: Theorem in_split_l_if : forall (A B : Type)(ls : list (A * B)) a, In a (fst (split ls)) -> exists b, In (a, b) ls.
proof: Proof. induction ls; intuition; simpl in *. intuition. remember (split ls) as z. destruct z. simpl in *. intuition. subst. econstructor; intuition. edestruct IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation