proposition: Lemma inl_map_property_res1 S u F g i x: inl_map_compat S u F -> inl_map_property S u F g -> inc i (isI S) -> inc x (Vg (isE S) i) -> Vf g (class (inl_equiv S) (J x i)) = Vf (Vg u i) x.
proof: Proof. move => [p1 p2 p3 p4] [[fg sg tg] hb] hc hd. move:(inl_can_fun_fp hc) => [fc sc tc]. have co: g \coP inl_can_fun S i by split => //; ue. have xs: inc x (source (inl_can_fun S i)) by ue. rewrite (hb _ hc); rewrite compfV//. by rewrite /inl_can_fun LfV//; apply: inl_can_fun_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)