proposition: Lemma PermutationA_app_head l₁ l₂ k : PermutationA l₁ l₂ → PermutationA (k ++ l₁) (k ++ l₂).
proof: Proof. intros. induction k. easy. apply permA_skip; intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads