proposition: Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
proof: Proof. simpl. apply elem_of_list_bind. exists (y :: l). split; simpl. - destruct l; csimpl; rewrite !elem_of_cons; auto. - apply elem_of_list_bind. simpl. eauto using interleave_cons, permutations_refl. Qed.
imports: stdpp(options)