proposition: Lemma consn_app : forall ll1 ll2, consn (ll1 ++ ll2) = consn ll1 ++ consn ll2.
proof: Proof. intros ll1; induction ll1 as [ | [a la] ll1]; simpl; trivial; simpl; intros; rewrite IHll1; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)