proposition: Lemma can_vset' : cancel imfset_bij_bwd imfset_bij_fwd.
proof: Proof. move => [x Hx]. rewrite /imfset_bij_fwd /imfset_bij_bwd. apply: val_inj => /=. by rewrite (tagged (imfset_inv [` Hx])). Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)