proposition: Lemma permut_consn : forall ll1 ll2, LLP.permut ll1 ll2 -> permut (consn ll1) (consn ll2).
proof: Proof. intros ll1; induction ll1 as [ | [a la] ll1]; simpl; intros ll2 P. rewrite (permut_nil (LLP.permut_sym P)); simpl; auto. assert (ala_in_ll2 : In (a,la) ll2). rewrite <- (in_permut_in P); left; trivial. destruct (In_split _ _ ala_in_ll2) as [ll2' [ll2'' H]]; subst. rewrite <- LLP.permut_cons_inside in P. rewrite consn_app; simpl; rewrite <- permut_cons_inside. rewrite <- consn_app; apply IHll1; trivial. apply (equiv_refl _ _ eq_proof). apply (equiv_refl _ _ LEDS.eq_proof). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)