proposition: Lemma lge_trans: forall (G1 G2 G3: Graph), labeled_graph_equiv G1 G2 -> labeled_graph_equiv G2 G3 -> labeled_graph_equiv G1 G3.
proof: Proof. intros; destruct H as [? [? ?]], H0 as [? [? ?]]. split; [| split]. + transitivity G2; auto. + intros. assert (vvalid G2 v) by (pose proof (proj1 H v); tauto). specialize (H1 v H5 H7); specialize (H3 v H7 H6); congruence. + intros. assert (evalid G2 e) by (pose proof (proj1 (proj2 H) e); tauto). specialize (H2 e H5 H7); specialize (H4 e H7 H6); congruence. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.lib.Equivalence_ext