proposition: Lemma permut0_cons_inside : forall e1 e2 l l1 l2, eq_A e1 e2 -> (permut0 eq_A l (l1 ++ l2) <-> permut0 eq_A (e1 :: l) (l1 ++ e2 :: l2)).
proof: Proof. intros e1 e2 l l1 l2 e1_eq_e2. apply (permut0_add_inside nil l l1 l2 e1_eq_e2). Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)