proposition: Lemma bij_perm_enum (I1 I2 : finType) (f : bij I1 I2) : perm_eq (index_enum I2) [seq f i | i <- index_enum I1].
proof: Proof. exact: perm_index_enum. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)