proposition: Lemma hom2_sskel (G1 G2 : graph2) (h: iso2 G1 G2) : forall x y, @edge_rel (sskeleton G1) x y -> @edge_rel (sskeleton G2) (h x) (h y).
proof: Proof. apply sskelP. - move => x y. by rewrite sgP. - move => e He. rewrite /edge_rel /= [_ -- _](_ : _ = true) /= /edge_rel //=. rewrite /sk_rel /= bij_eq ?He //=. apply/existsP; exists (h.e e). rewrite !inE !endpoint_iso. case (h.d e)=>/=; by rewrite !eqxx. - move => H. by rewrite /edge_rel /= bij_eq // H iso2_input iso2_output !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)