proposition: Lemma in_in_split_set : forall (A : Type) (a b : A) (l1 l2 k1 k2 : list A), l1 ++ a :: l2 = k1 ++ b :: k2 -> {l | l1 = k1 ++ b :: l /\ k2 = l ++ a :: l2} + {l | k1 = l1 ++ a :: l /\ l2 = l ++ b :: k2} + {a = b /\ l1 = k1 /\ l2 = k2}.
proof: Proof. intros A a b l1; revert a b; induction l1 as [ | a1 l1]; intros a b l2 k1 k2 H; destruct k1 as [ | b1 k1]. simpl in H; injection H; intros l2_eq_k2 a_eq_b; right; repeat split; trivial. simpl in H; injection H; intros l2_eq_k a_eq_b1; subst; clear H. left; right; exists k1; repeat split; trivial. simpl in H; injection H; intros l_eq_k2 a1_eq_b; subst; clear H. left; left; exists l1; repeat split; trivial. simpl in H; injection H; intros l_eq_k a1_eq_b1; subst; clear H. destruct (IHl1 _ _ _ _ _ l_eq_k) as [[H | H] | H]. destruct H as [l [H1 H2]]; subst. left; left; exists l; repeat split; trivial. destruct H as [l [H1 H2]]; subst. left; right; exists l; repeat split; trivial. destruct H as [a_eq_b [H1 H2]]; subst. right; repeat split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)