proposition: Theorem listReplace_None_Permutation : forall (A : Set) n ls (y : A), nth n ls None = None -> Permutation (getSomes (listReplace ls n (Some y) None)) (y :: (getSomes ls)).
proof: Proof. induction n; intuition; simpl in *. destruct ls; simpl in *. eapply Permutation_refl. subst. eapply Permutation_refl. destruct ls; simpl in *. eapply (IHn nil). eapply nth_nil. destruct o. eapply Permutation_sym. eapply perm_trans. eapply perm_swap. eapply perm_skip. eapply Permutation_sym. eapply IHn. trivial. eapply IHn. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation