proposition: Lemma lp_graph_iso_trans: forall `(g1: @LabeledGraph V E EV EE DV DE DG) g2 g3, label_preserving_graph_isomorphism g1 g2 -> label_preserving_graph_isomorphism g2 g3 -> label_preserving_graph_isomorphism g1 g3.
proof: Proof. intros. destruct H as [v12 [v21 [e12 [e21 ?]]]]. destruct H0 as [v23 [v32 [e23 [e32 ?]]]]. exists (compose v23 v12), (compose v21 v32), (compose e23 e12), (compose e21 e32). eapply lp_graph_iso_exp_trans; eauto. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext