proposition: Lemma find_not_in_some: forall l1 l2 x li1 li2, findNotIn l1 l2 nil = (Some x, (li1, li2)) -> Forall (fun m => In m l2) li1 /\ l1 = li1 ++ x :: li2 /\ ~ In x li1 /\ ~ In x l2.
proof: Proof. intros. assert (Forall (fun m : V => In m l2) nil) by apply Forall_nil. destruct (find_not_in_some_explicit l1 l2 nil x li1 li2 H H0). destruct H2 as [? [l4 [? [? ?]]]]. simpl in H3. rewrite H3 in *. repeat split; auto. Qed.
imports: Coq.Classes.EquivDec CertiGraph.lib.List_ext