proposition: Lemma imset_bijT (aT rT : finType) (i : bij aT rT) : i @: setT = setT.
proof: Proof. by apply/setP => x; rewrite -[x in LHS](bijK' i) bij_imset_f !inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)