proposition: Lemma guarded_morphism_step: forall {PV: V -> Prop} {PE: E -> Prop} {vmap emap n m} {g: PreGraph V E} {g': PreGraph V' E'}, guarded_morphism PV PE vmap emap g g' -> Included (Intersection _ (weak_edge_prop PV g) (evalid g)) PE -> PV n -> PV m -> step g n m -> step g' (vmap n) (vmap m).
proof: Proof. intros. rewrite !@step_spec in H3 |- *. destruct H3 as [e [? [? ?]]]. exists (emap e). assert (PE e) by (apply H0; unfold Ensembles.In; rewrite Intersection_spec; subst; auto). split; [| split]. + eapply (evalid_preserved H); eauto. + symmetry; subst; eapply (src_preserved H); eauto. + symmetry; subst; eapply (dst_preserved H); eauto. 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation