proposition: Lemma hom_skel (G1 G2 : graph) (h: iso G1 G2) : {homo h : x y / (x : skeleton _) -- y}.
proof: Proof. apply: skelP. - move => x y. by rewrite sgP. - move => e He. rewrite /edge_rel/=/sk_rel. rewrite bij_eq ?He //=. apply/existsP; exists (h.e e). rewrite !inE !endpoint_iso /=. case (h.d e)=>/=; by rewrite !eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)