proposition: Lemma Permutation_PermutationA l₁ l₂ : Permutation l₁ l₂ -> PermutationA l₁ l₂.
proof: Proof. induction 1. - constructor. - now constructor. - apply permA_swap. - econstructor; eauto. Qed.
imports: Permutation SetoidList