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