proposition: Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
proof: Proof. revert l'. induction l as [|y l IH]; intros l'; simpl. - rewrite elem_of_list_singleton. by intros ->. - rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|]. rewrite (IH _ H). constructor. Qed.
imports: stdpp(options)