proposition: Lemma can_inj_imset (A : {set F}) : i @^-1: (i @: A) = A.
proof: Proof. by apply/setP => x; rewrite !inE (mem_imset). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)