proposition: Lemma permut0_cons : forall e1 e2 l1 l2, eq_A e1 e2 -> (permut0 eq_A l1 l2 <-> permut0 eq_A (e1 :: l1) (e2 :: l2)).
proof: Proof. intros e1 e2 l1 l2 e1_eq_e2; split; intro P. apply (@Pcons _ _ eq_A e1 e2 l1 (@nil A) l2); trivial. replace l2 with (nil ++ l2); trivial; apply permut_cons_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)