proposition: Lemma equiv_of_class (T : finType) (e : rel T) : equiv_class_of (equiv_of e).
proof: Proof. constructor; auto using equiv_of_refl, equiv_of_sym, equiv_of_trans. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)