proposition: Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
proof: Proof. split. - revert l'. induction l; simpl; intros l''. + rewrite elem_of_list_singleton. by intros ->. + rewrite elem_of_list_bind. intros [l' [Hl'' ?]]. rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto. - induction 1; eauto using permutations_refl, permutations_skip, permutations_swap, permutations_trans. Qed.
imports: stdpp(options)