proposition: Lemma inl_prop7_cor_ii (a := class (inl_equiv S') (J (Vg a_fam (rep (isI S))) (rep (isI S)))): Imf inl_p7c2_ip = Vfi1 (inductive_limit_fun S S' u) a.
proof: Proof. move:(inl_map2_prop sii m2c); set uu := (inductive_limit_fun S S' u). move =>[ [fuu suu tuu] uup]. have II:= (inl_same_index_same_I sii). set Nip:=(inl_sub_fam_im3). move: (inl_sub_fam_im4) => [[fi _] si ti]. move:(a_fam_prop) => [Ha Hb Hc Hd]. set_extens t. move/(Imf_P fi); rewrite si; move => [v va ->]. apply(iim_fun_set1_P _ fuu); rewrite suu. move/inductive_limit_hi: va => /= [Qr Pr ->]. rewrite (inl_subfam_prop3 inl_sub_fam_im3 Qr Pr). move: Pr; rewrite /inl_p7c2_Ni LgV//. move:(proj43 m2c _ Qr) => [fui sui tui]. move/(iim_fun_set1_P _ fui); rewrite sui; move => [ha hb]. split; first by apply: inl_class_in_lim. by rewrite (inl_map_val_aux2 sii m2c Qr ha) /a -(inl_sub_fam_im3_val Qr) hb. move/(iim_fun_set1_P _ fuu);rewrite suu. move => [/inductive_limit_hi [Qr Pr ->]]. move:(Qr); rewrite II => Qr'. have pa: inc (Vg a_fam (Q (rep t))) (Vg (isE S') (Q (rep t))) by apply: Hc. have pb: inc (Vf (Vg u (Q (rep t))) (P (rep t))) (Vg (isE S') (Q (rep t))). move:(proj43 m2c _ Qr) => [fui sui tui]; Wtac. rewrite (inl_map_val_aux2 sii m2c Qr Pr). rewrite /a -(inl_sub_fam_im3_val Qr). move/ (inl_class_eq_bis Qr' Qr' pa pb) => [j [_]]; aw => lij. move: (Hd _ lij); aw => ->; rewrite - sii in lij. rewrite (inl_map2_compat_prop0 sii m2c Pr lij). set y := Vf (Vg (isf S) (J (Q (rep t)) j)) (P (rep t)) => ya. move:(proj2 (inl_prop0 lij)) => jI. move:(proj43 m2c _ jI) => [fui sui tui]. have yNi: inc y (Vg inl_p7c2_Ni j). rewrite /y /inl_p7c2_Ni LgV//; apply/(iim_fun_set1_P _ fui); split => //. move: (inl_prop4 lij) => [fij sij tij]; rewrite sui; Wtac. rewrite -(inl_class_of_fij lij Pr). rewrite -(inl_subfam_prop3 inl_sub_fam_im3 jI yNi). apply/(Imf_P fi). exists (class (inl_equiv (inl_p7c2_S'')) (J y j)) => //;rewrite si. by apply:inl_class_in_lim. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)