proposition: Lemma inl_limit_fun_surj S S' u: inl_same_index S S' -> inl_map2_compat S S' u -> (forall i, inc i (isI S) -> surjection (Vg u i)) -> surjection (inductive_limit_fun S S' u).
proof: Proof. move => ha hb hc. move:(inl_map2_prop ha hb) => [[ff sf tf] etc]. split => //; rewrite tf sf => y /(inductive_limitP) [ry ->]. move:ry; rewrite inl_equiv_sr=> qa. move:(qa)=> /inl_sumP [pry Qry Pry]. have II:= (inl_same_index_same_I ha). rewrite - II in Qry. move: (hb) => [hb1 hb2 hb3 hb4]. move:(hb3 _ Qry) => [fui sui tui]. rewrite - tui in Pry. move:(proj2 (hc _ Qry) _ Pry); rewrite sui; move =>[x xs xv]. have cc: inc (class (inl_equiv S) (J x (Q (rep y)))) (inductive_limit S). by apply:inl_class_in_lim. by ex_tac; rewrite inl_map_val_aux2 // - xv pry. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)