proposition: Lemma guarded_bij_proper_aux1: forall PV PE vmap emap (G1 G2: PreGraph V E) (G1' G2': PreGraph V' E'), guarded_structurally_identical PV PE G1 G2 -> guarded_structurally_identical (image_set PV vmap) (image_set PE emap) G1' G2' -> guarded_bij PV PE vmap emap G1 G1' -> guarded_bij PV PE vmap emap G2 G2'.
proof: Proof. intros. split; intros. + apply (vmap_inj H1); auto. + apply (emap_inj H1); auto. + eapply guarded_morphism_proper_aux1; eauto. apply bij_is_morphism; 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