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