proposition: Lemma inl_map_surjective S u F: inl_map_compat S u F -> (surjection (inductive_map S u F) <-> F = unionf (isI S) (fun i => Imf (Vg u i))).
proof: Proof. move => h0; move:(inl_map_prop h0) => h1. move: (h1) => [[fu su tu] cu]. split => h2. move: (h0) => [fgu du uv1 uv2]. set_extens t. rewrite - tu => tt; move: (proj2 h2 _ tt); rewrite su;move => [x xs ->]. move/inductive_limit_hi: xs => [pa pb ->]; apply/setUf_P; ex_tac. rewrite (inl_map_property_res1 h0 h1 pa pb). move:(uv1 _ pa) => [fui sui tui]. apply/(Imf_P fui); rewrite sui; ex_tac. move/setUf_P => [i iI]. move:(uv1 _ iI) => [fui sui tui]. case/(Imf_P fui); rewrite sui => [x xE ->]; Wtac. split => //; rewrite tu su {1} h2 => y yF. move/setUf_P: yF => [i iI]. move: (h0) => [fgu du uv1 uv2]. move:(uv1 _ iI) => [fui sui tui]; move/(Imf_P fui); rewrite sui. move => [x xE ->]. exists (class (inl_equiv S) (J x i)); first by apply:inl_class_in_lim. symmetry; exact:(inl_map_property_res1 h0 h1 iI xE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)