proposition: Theorem nth_0_snd_split_cons : forall (A B : Type)(x : A * B)(ls: list (A * B)) def, nth 0 (snd (split (x :: ls))) def = (snd x).
proof: Proof. intuition idtac; simpl in *. remember (split ls) as z. destruct z. simpl. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation