proposition: Lemma interleave_interleave_toggle x1 x2 l1 l2 l3 : l1 ∈ interleave x1 l2 → l2 ∈ interleave x2 l3 → ∃ l4, l1 ∈ interleave x2 l4 ∧ l4 ∈ interleave x1 l3.
proof: Proof. revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl. { rewrite !elem_of_list_singleton. intros ? ->. exists [x1]. change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]). by rewrite (comm (++)), elem_of_list_singleton. } rewrite elem_of_cons, elem_of_list_fmap. intros Hl1 [? | [l2' [??]]]; simplify_eq/=. - rewrite !elem_of_cons, elem_of_list_fmap in Hl1. destruct Hl1 as [? | [? | [l4 [??]]]]; subst. + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto. + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto. + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons. - rewrite elem_of_cons, elem_of_list_fmap in Hl1. destruct Hl1 as [? | [l1' [??]]]; subst. + exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons, !elem_of_list_fmap. split; [| by auto]. right. right. exists (y :: l2'). rewrite elem_of_list_fmap. naive_solver. + destruct (IH l1' l2') as [l4 [??]]; auto. exists (y :: l4). simpl. rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver. Qed.
imports: stdpp(options)