proposition: Lemma list_sim_permutation : forall l l' m, list_simA l l' -> permutation eqA_dec l m -> exists m', list_simA m m' /\ permutation eqA_dec l' m'.
proof: Proof. unfold Setoid_Theory in eqA_Equivalence. induction l; intros. exists (nil (A:=A)); split. destruct m. constructor. set (w := H0 a); inversion w. destruct (eqA_dec a a). lia. absurd (eqA a a); intuition. inversion H. apply permut_refl. destruct l'. inversion H. destruct (permutation_cons eqA_Equivalence H0) as [p [a' [mp [aa' lm]]]]. destruct (IHl l' (drop_nth m p)) as [m' [mm' l'm']]; trivial. inversion H; trivial. assert (length m' >= p). rewrite <- (list_sim_length mm'). set (h := nth_some m p mp). set (w := drop_nth_length m p). lia. exists (insert_nth m' p a0); split. unfold list_simA; apply list_sim_insert_nth with p a' a0; trivial. apply nth_insert_nth; trivial. apply P_eqA_comp with a a0; intuition. inversion H; intuition. rewrite drop_nth_insert_nth; trivial. apply permutation_sym. apply insert_nth_permut'. apply permutation_sym; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)