proposition: Lemma ex9_map_property_res1 g i x: ex9_map_property g -> inc i I -> inc x (Vg E i) -> Vf g (class ex9_rels_ext (J x i)) = Vf (Vg u i) x.
proof: Proof. move =>[[fg sg tg] hb] hc hd. move:(ex9_can_fun_fp hc) => [fc sc tc]. have co: g \coP ex9_can_fun i by split => //; ue. have xs: inc x (source (ex9_can_fun i)) by ue. rewrite (hb _ hc) compfV//. by rewrite /ex9_can_fun LfV//; apply: ex9_can_fun_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)