proposition: Lemma can_vset : cancel imfset_bij_fwd imfset_bij_bwd.
proof: Proof. move => x. rewrite /imfset_bij_fwd /imfset_bij_bwd /=. set S := Sub _ _. apply: g_inj. by rewrite (tagged (imfset_inv S)). Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)