proposition: Lemma guarded_morphism_reachable: 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 -> reachable_by g n PV m -> reachable g' (vmap n) (vmap m).
proof: Proof. intros. rewrite reachable_by_eq_partialgraph_reachable in H1. pattern m. eapply (@reachable_general_ind V E) with (x := n); [| exact H1 |]. + intros. apply reachable_edge with (vmap x); auto. rewrite <- partialgraph_edge_iff in H2. destruct H2 as [? [? ?]]. eapply guarded_morphism_edge; eauto. + apply reachable_refl. rewrite <- reachable_by_eq_partialgraph_reachable in H1. eapply (vvalid_preserved H); eauto. - apply reachable_by_head_prop in H1; auto. - apply reachable_by_head_valid in H1; 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation