proposition: Fact list_split_middle X l1 (x1 : X) r1 l2 x2 r2 : ~ In x1 l2 -> ~ In x2 l1 -> l1++x1::r1 = l2++x2::r2 -> l1 = l2 /\ x1 = x2 /\ r1 = r2.
proof: Proof. intros H1 H2 H. apply list_app_eq_inv in H. destruct H as [ (m & H3 & H4) | (m & H3 & H4) ]; destruct m. inversion H4; subst; rewrite app_nil_r; auto. inversion H4; subst; destruct H1; apply in_or_app; right; left; auto. inversion H4; subst; rewrite app_nil_r; auto. inversion H4; subst; destruct H2; apply in_or_app; right; left; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)