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