fact: Fixpoint findNotIn (l1 l2 l3: list V) : (option V * (list V * list V)) := match l1 with | nil => (None, (nil, nil)) | x :: l => if (in_dec equiv_dec x l2) then findNotIn l l2 (x :: l3) else (Some x, (rev l3, l)) end.
imports: Coq.Classes.EquivDec CertiGraph.lib.List_ext