proposition: Lemma pregraph_join_empty_single: forall v0 src0 dst0, pregraph_join (eq v0) (Empty_set _) (empty_pregraph src0 dst0) (single_vertex_pregraph v0).
proof: Proof. intros. unfold empty_pregraph, single_vertex_pregraph. split; [| split; [| split]]; simpl. + split; intros. - destruct_eq_dec v0 a; tauto. - auto. + split; intros. - tauto. - auto. + intros; tauto. + intros; tauto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 Coq.Lists.List CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen