proposition: Lemma hom_eqL (V : finType) (e1 e2 : rel V) (G : sgraph) (h : V -> G) (e1_sym : symmetric e1) (e1_irrefl : irreflexive e1) (e2_sym : symmetric e2) (e2_irrefl : irreflexive e2): e1 =2 e2 -> @hom_s (SGraph e1_sym e1_irrefl) G h -> @hom_s (SGraph e2_sym e2_irrefl) G h.
proof: Proof. move => E hom_h x y. rewrite /edge_rel/= -E. exact: hom_h. Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)