proposition: Lemma efun_of_bij (F G : pre_graph) (i : F ⩭2 G) : exists g, [/\ {in eset F, cancel (efun_of i) g}, {in eset G, cancel g (efun_of i)} & {in eset G, forall x, g x \in eset F}].
proof: Proof. case: i => isF isG i /=. pose g := efun_body (iso2_sym i).e. exists g. split => //; rewrite /efun_of/=. - move => e Fe. rewrite /g !efun_bodyE /=. exact: valP. move => p. by rewrite fsvalK bijK. - move => e Ge. rewrite /g !efun_bodyE /=. exact: valP. move => p. by rewrite fsvalK bijK'. - move => e Ge. rewrite /g !efun_bodyE /=. exact: valP. Qed.
imports: Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(rewriting open_confluence finmap_plus)