proposition: Lemma ihom_hom (F G: graph) (hv: bij F G) (he: (edge F) -> (edge G)) hd : is_ihom hv he hd -> is_hom hv he hd.
proof: Proof. move => [? H ?]. split => // v. by rewrite big_bij_eq -H bijK'. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)