proposition: Lemma is_null_dec: forall x, {is_null x} + {~ is_null x}.
proof: Proof. intros. destruct is_null as [P ?]. simpl. auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen