proposition: Lemma hom_id G: @is_hom G G id id xpred0.
proof: Proof. split => // v. by rewrite big_pred1_eq. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)