proposition: Lemma inl_limit_fun_inj S S' u: inl_same_index S S' -> inl_map2_compat S S' u -> (forall i, inc i (isI S) -> injection (Vg u i)) -> injection (inductive_limit_fun S S' u).
proof: Proof. move => ha hb hc. have II:= (inl_same_index_same_I ha). move:(inl_map2_prop ha hb) => [[ff sf tf] etc]. move: (hb) => [hb1 hb2 hb3 hb4]. split => //; rewrite sf => x y xs ys. move/inductive_limit_hi: xs => [Qrx Prx ->]. move/inductive_limit_hi: ys => [Qry Pry ->]. rewrite (inl_map_val_aux2 ha hb Qrx Prx) (inl_map_val_aux2 ha hb Qry Pry). set xx := (Vf (Vg u (Q (rep x))) _). set yy := (Vf (Vg u (Q (rep y))) _). have xxE: inc xx (Vg (isE S') (Q (rep x))). rewrite /xx;move:(hb3 _ Qrx) => [ff' sf' tf']; Wtac. have yyE: inc yy (Vg (isE S') (Q (rep y))). rewrite /yy;move:(hb3 _ Qry) => [ff' sf' tf']; Wtac. rewrite II in Qrx Qry. move/(inl_class_eq_bis Qrx Qry xxE yyE) => [k []]; aw; rewrite - ha => lik ljk. rewrite (inl_map2_compat_prop0 ha hb Prx lik). rewrite (inl_map2_compat_prop0 ha hb Pry ljk). rewrite - (inl_class_of_fij lik Prx) - (inl_class_of_fij ljk Pry). have kI := (proj2(inl_prop0 lik)). move:(inl_prop4 lik) => [fij sik tik]. move:(inl_prop4 ljk) => [fjj sjk tjk]. move: (hb3 _ kI) => [fuk suk tuk]. have qg: inc (Vf (Vg (isf S) (J (Q (rep x)) k)) (P (rep x))) (source (Vg u k)). rewrite suk. Wtac. have qh: inc (Vf (Vg (isf S) (J (Q (rep y)) k)) (P (rep y))) (source (Vg u k)). rewrite suk; Wtac. by move/(proj2 (hc _ (proj2(inl_prop0 lik))) _ _ qg qh) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)