proposition: Lemma merge_nothing': merge F r ≃ F.
proof: Proof. apply merge_surj with id id bij_id xpred0 =>//. - intros. apply Bool.iff_reflect. split. intros ->. by rewrite equiv_refl. intro E. apply H. by rewrite E. - exact: hom_id. Defined.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)