proposition: Lemma list_sim_insert_nth : forall p l l' a a', nth_error l p = Some a -> nth_error l' p = Some a' -> R a a' -> list_sim (drop_nth l p) (drop_nth l' p) -> list_sim l l'.
proof: Proof. induction p; intros. destruct l; destruct l'. constructor. inversion H2; discr. inversion H2; discr. constructor. inversion H; inversion H0; trivial. rewrite !drop_nth_cons in H2; trivial. destruct l; destruct l'. constructor. inversion H2; discr. inversion H2; discr. rewrite !drop_nth_succ in H2. inversion H2. constructor; trivial. apply IHp with a a'; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)