proposition: Lemma permutations_interleave_toggle x l1 l2 l3 : l1 ∈ permutations l2 → l2 ∈ interleave x l3 → ∃ l4, l1 ∈ interleave x l4 ∧ l4 ∈ permutations l3.
proof: Proof. revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl. { rewrite elem_of_list_singleton. intros Hl1 ->. eexists []. by rewrite elem_of_list_singleton. } rewrite elem_of_cons, elem_of_list_fmap. intros Hl1 [? | [l2' [? Hl2']]]; simplify_eq/=. - rewrite elem_of_list_bind in Hl1. destruct Hl1 as [l1' [??]]. by exists l1'. - rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind. destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto. destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto. Qed.
imports: stdpp(options)