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