proposition: Lemma find_not_in_none: forall l1 l2 l3, fst (findNotIn l1 l2 l3) = None -> Forall (fun m => In m l2) l1.
proof: Proof. induction l1; intros. apply Forall_nil. simpl in H. destruct (in_dec equiv_dec a l2). apply Forall_cons. auto. apply IHl1 with (a :: l3); auto. inversion H. Qed.
imports: Coq.Classes.EquivDec CertiGraph.lib.List_ext