proposition: Lemma inl_prop7_cor_i: Imf inl_p7c1_ji_lim' = Vfs (inductive_limit_fun S S' u) (Imf inl_p7c1_ji_lim).
proof: Proof. move: inl_p7c1_ji_prop => [[fci _] sci tci]. move: inl_p7c1_ji'_prop => [[fci' _] sci' tci']. have II:= (inl_same_index_same_I sii). move:(inl_map2_prop sii m2c); set uu := (inductive_limit_fun S S' u). move =>[ [fuu suu tuu] uup]. have ha:sub (Imf inl_p7c1_ji_lim) (source uu). move => t/(Imf_P fci); rewrite sci suu. move => [v/inductive_limit_hi /= [Qi Pm ->] ->]. rewrite (inl_subfam_prop3 _ Qi Pm). by apply:inl_class_in_lim => //; apply:(proj43 Mhyp _ Qi). move:m2c => [fgu du up1 up2]. set_extens t. move/(Imf_P fci'); rewrite sci'. move => [v /inductive_limit_hi /= [Qi' Pm ->] ->]. rewrite (inl_subfam_prop3 _ Qi' Pm). have Qi:inc (Q (rep v)) (isI S) by rewrite II. move: Pm; rewrite /inl_p7c1_M' LgV//. move:(up1 _ Qi) => [fui sui tui]. have hb: sub (Vg M (Q (rep v))) (source (Vg u (Q (rep v)))). rewrite sui; apply: (proj43 Mhyp _ Qi). move/(Vf_image_P fui hb) => [y yM ->]. rewrite -(inl_map_val_aux2 sii m2c Qi ((proj43 Mhyp _ Qi) _ yM)). have hc: inc (class (inl_equiv S) (J y (Q (rep v)))) (Imf inl_p7c1_ji_lim). apply /(Imf_P fci); rewrite sci. exists (class (inl_equiv inl_p7c1_MS) (J y (Q (rep v)))). by apply:inl_class_in_lim. by rewrite inl_subfam_prop3. apply/(Vf_image_P fuu ha); ex_tac. move/(Vf_image_P fuu ha) => [v /(Imf_P fci)]; rewrite sci. move => [w /inductive_limit_hi /= [Qi Pcv ->] ->]. have hb: inc (P (rep w)) (Vg (isE S) (Q (rep w))). by apply: (proj43 Mhyp _ Qi). rewrite (inl_subfam_prop3 _ Qi Pcv) inl_map_val_aux2 // => ->. apply/(Imf_P fci'); rewrite sci'. have Qi': inc (Q (rep w)) (isI S') by ue. move:(up1 _ Qi) => [fu su tu]. set y := (Vf (Vg u (Q (rep w))) (P (rep w))). have hc:sub (Vg M (Q (rep w))) (source (Vg u (Q (rep w)))). rewrite su; apply:(proj43 Mhyp _ Qi). have yc: inc y (Vg inl_p7c1_M' (Q (rep w))). rewrite /inl_p7c1_M' LgV//; apply/(Vf_image_P fu hc); ex_tac. exists (class (inl_equiv inl_p7c1_MS') (J y (Q (rep w)))). apply: inl_class_in_lim => //=. by rewrite inl_subfam_prop3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)