proposition: Lemma lp_graph_iso_exp_trans: forall `(g1: @LabeledGraph V E EV EE DV DE DG) g2 g3 v12 v21 e12 e21 v23 v32 e23 e32, label_preserving_graph_isomorphism_explicit g1 g2 v12 v21 e12 e21 -> label_preserving_graph_isomorphism_explicit g2 g3 v23 v32 e23 e32 -> label_preserving_graph_isomorphism_explicit g1 g3 (compose v23 v12) (compose v21 v32) (compose e23 e12) (compose e21 e32).
proof: Proof. intros. destruct H, H0. split; intros; [|unfold compose..]. - eapply pregraph_iso_exp_trans; eauto. - destruct lp_pregraph_iso0. rewrite vlabel_iso0, vlabel_iso1; auto. - destruct lp_pregraph_iso0. rewrite elabel_iso0, elabel_iso1; auto. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext