proposition: Theorem nth_snd_split_app_gen : forall (A B : Type)(ls1 ls2 : list (A * B)) n def, n = length ls1 -> nth n (snd (split (ls1 ++ ls2))) def = nth 0 (snd (split ls2)) def.
proof: Proof. intuition idtac; subst. eapply nth_snd_split_app. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation