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