proposition: Lemma map_pairs_id {A} (l: pairs A): map_pairs id l = l.
proof: Proof. elim l=>//=[[a a'] q]/=. congruence. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)