proposition: Lemma insert_2 : forall (A : Type) (l1 l2 r1 r2 r3 : list A) (a b b' : A), l1 ++ l2 = r1 ++ b :: r2 ++ b' :: r3 -> exists r1', exists r2', exists r3', l1 ++ a :: l2 = r1' ++ b :: r2' ++ b' :: r3'.
proof: Proof. intros A l1; induction l1 as [ | a1 l1]. simpl; intros l2 r1 r2 r3 a b b' H; rewrite H; exists (a :: r1); exists r2; exists r3; simpl; trivial. intros l2 [ | b1 r1] r2 r3 a b b' H; simpl in H; injection H; clear H; intros H a1_eq; subst a1. destruct (insert_1 l1 l2 r2 r3 a b' H) as [r2' [r3' H']]; simpl; rewrite H'. exists (@nil A); exists r2'; exists r3'; simpl; trivial. destruct (IHl1 l2 r1 r2 r3 a b b' H) as [r1' [r2' [r3' H']]]; simpl; rewrite H'. exists (b1 :: r1'); exists r2'; exists r3'; simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)