proposition: Lemma PermutationA_app_tail l₁ l₂ k : PermutationA l₁ l₂ → PermutationA (l₁ ++ k) (l₂ ++ k).
proof: Proof. intros E. now rewrite E. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads