proposition: Lemma lp_graph_iso_syn: forall `(g: @LabeledGraph V E EV EE DV DE DG) g', label_preserving_graph_isomorphism g g' -> label_preserving_graph_isomorphism g' g.
proof: Proof. intros. destruct H as [vmap [vmap' [emap [emap' ?]]]]. exists vmap', vmap, emap', emap. eapply lp_graph_iso_exp_sym; eauto. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext