fact: Definition fsetU1_fun (a : (x |` A)) : (y |`B) := match fset1UE (fsvalP a) with | inl _ => Sub y fset1U1 | inr (_,p) => Sub (val (f [` p])) (fset1Ur (valP (f [` p]))) end.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)