proposition: Lemma equiv_comp_pi (x: T): repr (repr (pi e' (pi e x))) = x %[mod equiv_comp].
proof: Proof. apply/eqquotP. rewrite /equiv_comp map_equivE reprK. apply: piK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)