proposition: Theorem listReplace_getSomes_Permutation_h : forall (A : Set) l1' l2, Permutation l1' l2 -> forall l1 n2 (y : A), l1' = getSomes l1 -> nth n2 l1 None = None -> Permutation (getSomes (listReplace l1 n2 (Some y) None)) (y :: l2).
proof: Proof. induction 1; intuition. eapply perm_trans. eapply listReplace_None_Permutation. trivial. rewrite <- H. eapply Permutation_refl. eapply perm_trans. eapply listReplace_None_Permutation. trivial. rewrite <- H0. eapply perm_skip. eapply perm_skip. trivial. eapply perm_trans. eapply listReplace_None_Permutation. trivial. rewrite <- H. eapply perm_skip. eapply perm_swap. eapply perm_trans. eapply listReplace_None_Permutation. trivial. rewrite <- H1. eapply perm_skip. eapply perm_trans. eapply H. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation