proposition: Lemma rep_sys_function_pr2 g f x: injection g -> function f -> partition_w_fam (graph f) x -> sub (target g) x -> (forall i, inc i (source f) -> exists! a, (inc a (source g) /\ inc (Vf g a) (Vf f i))) -> representative_system_function g f x.
proof: Proof. move=> ig ff pf stx exu; move:(ig)=> [fg _]. split =>//; split=>//; first by apply:(sub_trans (Imf_Starget fg) stx). move=> i isf; move: (exu _ isf) => [a [[asg Wa] un]]. exists (Vf g a); set_extens t. move/setI2_P => [tv /(Imf_P fg) [z zsg eq]]; apply/set1_P. by rewrite eq;congr (Vf g _); symmetry;apply: un;rewrite - eq. move /set1_P => ->; apply/setI2_P; split => //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)