proposition: Lemma pregraph_iso_exp_trans: forall `(g1: @PreGraph V1 E1 EV1 EE1) `(g2: @PreGraph V2 E2 EV2 EE2) `(g3: @PreGraph V3 E3 EV3 EE3) v12 v21 e12 e21 v23 v32 e23 e32, pregraph_isomorphism_explicit g1 g2 v12 v21 e12 e21 -> pregraph_isomorphism_explicit g2 g3 v23 v32 e23 e32 -> pregraph_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..]; auto. - eapply bijective_trans; auto. - eapply bijective_trans; auto. - rewrite <- src_bij1, <- src_bij0; auto. - rewrite <- dst_bij1, <- dst_bij0; auto. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext