proposition: Lemma rep_sys_function_pr g f x i: representative_system_function g f x -> inc i (source f) -> exists! a, (inc a (source g) /\ inc (Vf g a) (Vf f i)).
proof: Proof. move=> [[fg ig] [ff pf gg alsi]] ins. move: (alsi _ ins) => [u isu]. apply /unique_existence; split. move: (set1_1 u). rewrite - isu; move /setI2_P => [pa] /(Imf_P fg) [a asg pb]. by exists a; rewrite - pb. move=> a b [asg Wa][bsg Wb]; apply: ig => //. have aux: (forall a, inc a (source g) -> inc (Vf g a) (Vf f i) -> Vf g a = u). move=> c csg Wc. apply: set1_eq; rewrite -isu; apply: setI2_i => //; Wtac. rewrite aux // aux //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)