proposition: Lemma guarded_morphism_proper_aux3: forall PV1 PV2 PE1 PE2 vmap emap (G: PreGraph V E) (G': PreGraph V' E'), Same_set PV1 PV2 -> Same_set PE1 PE2 -> guarded_morphism PV1 PE1 vmap emap G G' -> guarded_morphism PV2 PE2 vmap emap G G'.
proof: Proof. intros. rewrite Same_set_spec in *. split; intros. + apply (vvalid_preserved H1), H; auto. + apply (evalid_preserved H1), H0; auto. + apply (src_preserved H1); auto. - apply H0; auto. - apply H; auto. + apply (dst_preserved H1); auto. - apply H0; auto. - apply H; 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