proposition: Lemma partition_fun_fb: (allf (graph f) nonempty) -> bijection (Lf (Vf f) (source f) (quotient (partition_relation f x))).
proof: Proof. move: isc_rel_equivalence => er. rewrite /allf - (proj33 ff); move=> alne; apply: lf_bijective. - move=> t tf; apply/(setQ_P er). apply: isc_rel_class2 =>//; apply: (alne _ tf). - move=> u v us vs sW. move: (alne _ us)=> [y yu]; have yv: (inc y (Vf f v)) by rewrite - sW. by apply: (partition_inc_unique1 us yu vs yv). - move=> y; move/(setQ_P er) => ic. move: (isc_rel_class ic) => [u us] ->; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)