proposition: Lemma find_not_in_some_explicit: forall l1 l2 l3 x li1 li2, findNotIn l1 l2 l3 = (Some x, (li1, li2)) -> (Forall (fun m => In m l2) l3) -> (~ In x li1) /\ (~ In x l2) /\ exists l4, li1 = rev l3 ++ l4 /\ Forall (fun m => In m l2) l4 /\ l1 = l4 ++ x :: li2.
proof: Proof. induction l1; intros; simpl in H. inversion H. destruct (in_dec equiv_dec a l2). assert (Forall (fun m : V => In m l2) (a :: l3)) by (apply Forall_cons; auto). specialize (IHl1 l2 (a :: l3) x li1 li2 H H1). destruct IHl1 as [? [? [l4 [? [? ?]]]]]. split; auto. split; auto. exists (a :: l4). repeat split; auto. simpl in H4. rewrite <- app_assoc in H4. rewrite <- app_comm_cons in H4. rewrite app_nil_l in H4. auto. rewrite H6; apply app_comm_cons. inversion H. split. intro; apply n. rewrite Forall_forall in H0. apply (H0 a). rewrite H2. rewrite in_rev. auto. split. rewrite <- H2. auto. exists nil. repeat split; auto. rewrite app_nil_r. auto. Qed.
imports: Coq.Classes.EquivDec CertiGraph.lib.List_ext