proposition: Lemma list_permut_add_inside : forall a l1 l2 l3 l4, list_permut (l1 ++ l2) (l3 ++ l4) -> list_permut (l1 ++ a :: l2) (l3 ++ a :: l4).
proof: Proof. intros a l1 l2 l3 l4; unfold list_permut, meq; simpl; intros H b; generalize (H b); clear H; repeat rewrite multiplicity_app; simpl; intro H; rewrite Nat.add_comm; rewrite <- Nat.add_assoc; apply sym_eq; rewrite Nat.add_comm; rewrite <- Nat.add_assoc; apply (f_equal (fun n => match eq_elt_dec a b with | left _ => 1 | right _ => 0 end + n)); rewrite Nat.add_comm; rewrite <- H; apply Nat.add_comm. Qed.
imports: Coq(List Multiset Arith Setoid) hydras(decidable_set more_list)