proposition: Lemma imfset_bij_bwdE x p : imfset_bij_bwd (Sub (g x) p) = x.
proof: Proof. rewrite /imfset_bij_bwd. set t := imfset_inv _. by move/g_inj : (tagged t). Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)