proposition: Lemma guarded_morphism_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_morphism PV PE vmap emap G1 G1' -> guarded_morphism PV PE vmap emap G2 G2'.
proof: Proof. intros. destruct (proj1 (guarded_si_spec _ _ _ _) H) as [? [? [? ?]]]. destruct (proj1 (guarded_si_spec _ _ _ _) H0) as [? [? [? ?]]]. assert (forall v : V, PV v -> (vvalid G2 v <-> vvalid G2' (vmap v))). 1: { intros. rewrite <- H2 by auto. rewrite <- H6 by (constructor; auto). apply (vvalid_preserved H1); auto. } assert (forall e : E, PE e -> (evalid G2 e <-> evalid G2' (emap e))). 1: { intros. rewrite <- H3 by auto. rewrite <- H7 by (constructor; auto). apply (evalid_preserved H1); auto. } split; auto; intros. + assert (evalid G1 e) by (rewrite H3 by auto; auto). rewrite <- H8. 2: constructor; auto. 2: rewrite <- (evalid_preserved H1), H3 by auto; auto. 2: rewrite <- H11 by auto; auto. rewrite <- H4 by auto. apply (src_preserved H1); auto. rewrite H4 by auto; auto. + assert (evalid G1 e) by (rewrite H3 by auto; auto). rewrite <- H9. 2: constructor; auto. 2: rewrite <- (evalid_preserved H1), H3 by auto; auto. 2: rewrite <- H11 by auto; auto. rewrite <- H5 by auto. apply (dst_preserved H1); auto. rewrite H5 by auto; 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