proposition: Lemma PermutationA_app_comm l₁ l₂ : PermutationA (l₁ ++ l₂) (l₂ ++ l₁).
proof: Proof. induction l₁. - now rewrite app_nil_r. - rewrite <-app_comm_cons, IHl₁, app_comm_cons. now rewrite PermutationA_cons_append, <-app_assoc. Qed.
imports: Permutation SetoidList