proposition: Lemma lp_graph_iso_exp_refl: forall `(g: @LabeledGraph V E EV EE DV DE DG), label_preserving_graph_isomorphism_explicit g g id id id id.
proof: Proof. intros; split; auto. apply pregraph_iso_exp_refl. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext