proposition: Lemma aux05: forall e, PE3_root e -> src g e = root.
proof: Proof. intros. assert (In e es) by (rewrite H_ES; subst PE3_root; rewrite in_app_iff in H |- *; simpl in H |- *; tauto). rewrite H_OUT_EDGE in H0. destruct H0. auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism