proposition: Lemma permut_add_inside : forall e1 e2 l1 l2 l3 l4, eq_A e1 e2 -> (permut (l1 ++ l2) (l3 ++ l4) <-> permut (l1 ++ e1 :: l2) (l3 ++ e2 :: l4)).
proof: Proof. intros e1 e2 l1 l2 l3 l4 e1_eq_e2; split; intro P. apply permut_strong; trivial. apply permut_add_inside with e1 e2; trivial. intros a1 b1 a2 b2 _ _ _ _ a1_eq_b1 a2_eq_b1 a2_eq_b2; transitivity a2; trivial. transitivity b1; trivial. symmetry; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)