proposition: Lemma PermutationA_cons_app l l₁ l₂ x : PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂).
proof: Proof. intros E. rewrite E. now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc. Qed.
imports: Permutation SetoidList