proposition: Theorem snd_split_nil_if : forall (A B : Type)(ls : list (A * B)), snd (split ls) = nil -> ls = nil.
proof: Proof. induction ls; intuition idtac; simpl in *. destruct a. remember (split ls) as z. destruct z. simpl in *. discriminate. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation