fact: Parameter 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)).
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)