proposition: Lemma aux10: Disjoint _ PE3 (eq e0).
proof: Proof. intros. rewrite Disjoint_spec. intros e ? ?. subst e. assert (In e0 es) by (rewrite H_ES; rewrite in_app_iff; simpl; tauto). rewrite H_OUT_EDGE in H0. unfold out_edges in H0. destruct H0. subst PE3. rewrite Intersection_spec in H. unfold weak_edge_prop in H. rewrite H1 in H. destruct H as [? _]. subst PV3. apply reachable_by_through_set_foot_prop in H. subst M0. apply H; unfold Ensembles.In; rewrite Union_spec; right; 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