proposition: Lemma inl_sub_fam_im2 Mi (Mi' := Lg (isI S) (fun i => Vfi (Vg u i) (Vg Mi i))): inl_inv_image_compat Mi -> inl_subfam_hyp S Mi'.
proof: Proof. move:m2c => [ha hb hc hd] [qa qb qc qd]. have II:= (inl_same_index_same_I sii). rewrite/Mi'; split => //; fprops; aw; trivial. move => i iI;rewrite LgV//. move: (hc _ iI) => [fu su tu]; rewrite - su; apply:(sub_inv_im_source fu). by rewrite tu; apply: qc; rewrite - II. move => i j lij. move:(inl_prop0 lij) => [iI jI]; rewrite !LgV//. move => t. move: (hc _ iI) => [fui sui tui]. move: (hc _ jI) => [fuj suj tuj]. move:(inl_prop4 lij) => [fij sij tij]. rewrite - II in qc. have pa:sub (Vfi (Vg u i) (Vg Mi i)) (source (Vg (isf S) (J i j))). rewrite sij - sui; apply:(sub_inv_im_source fui); rewrite tui; fprops. move/(Vf_image_P fij pa) => [v /iim_fun_P [w wa wb] ->]. move:(hd _ _ lij) => hd'. rewrite sii in lij; move:(qd _ lij); aw => eqa. move:(inl_prop4 lij) => [fij' sij' tij']. have pb:sub (Vg Mi i) (source (Vg (isf S') (J i j))) by rewrite sij'; apply: qc. have pc:inc (Vf (Vg (isf S') (J i j)) w) (Vg Mi j). apply: eqa; apply/(Vf_image_P fij' pb); ex_tac. move:(p1graph_source fui wb); rewrite sui => pd. have aa :gle (isr S) i j by rewrite sii. apply/iim_fun_P; ex_tac. move:(inl_map2_compat_prop0 sii m2c pd aa); rewrite (Vf_pr fui wb) => ->. apply: (Vf_pr3 fuj);rewrite suj; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)