proposition: Lemma boundary_dst_consistent_si: forall (PE1: E -> Prop) (PV1 PV2: V -> Prop) vmap emap G G1' G2', guarded_morphism PV1 PE1 vmap emap G G1' -> guarded_morphism PV1 PE1 vmap emap G G2' -> boundary_dst_consistent PE1 PV2 vmap emap G G1' -> guarded_structurally_identical (image_set PV1 vmap) (image_set PE1 emap) G1' G2' -> boundary_dst_consistent PE1 PV2 vmap emap G G2'.
proof: Proof. intros. hnf in H |- *. intros. rewrite (H1 e) by auto; clear H1. rewrite guarded_si_spec in H2. destruct H2 as [? [? [? ?]]]. apply H7. + constructor; auto. + rewrite <- (evalid_preserved H); auto. + rewrite <- (evalid_preserved 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.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation