proposition: Lemma permut_app_inv2 : forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
proof: Proof. intros l l1 l2; unfold permutation, meq; simpl; intros H a; generalize (H a); clear H. do 2 rewrite list_contents_app. simpl. lia. Qed.
imports: Lia Relations Multiset SetoidList