proposition: Lemma inl_sub_fam_im1: inl_subfam_hyp S' inl_p7c1_M'.
proof: Proof. have II:= (inl_same_index_same_I sii). move: m2c => [ha hb hc hd]. move: Mhyp => [qa qb qc qd]. rewrite /inl_p7c1_M'; split; aww. rewrite - II => i iI; rewrite LgV//. move: (hc _ iI) => [fui sui tui]. rewrite - tui; apply:(fun_image_Starget1 fui). rewrite - sii => 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:(hd _ _ lij) (qd _ _ lij) => hd' qd'. move:(inl_prop4 lij) => [fij sij tij]. rewrite sii in lij. move:(inl_prop4 lij) => [fij' sij' tij']. have pa: sub (Vfs (Vg u i) (Vg M i)) (source (Vg (isf S') (J i j))). rewrite sij' - tui; apply:(fun_image_Starget1 fui). have pb: sub (Vg M j) (source (Vg u j)) by rewrite suj; apply: qc. have pc: sub (Vg M i) (source (Vg u i)) by rewrite sui; apply: qc. move/(Vf_image_P fij' pa) => [v /(Vf_image_P fui pc) [w wa ->] ->]. have co1: Vg u j \coP Vg (isf S) (J i j) by split => //;ue. have co2: Vg (isf S') (J i j) \coP Vg u i by split => //; ue. have ws0: inc w (source (Vg u i)) by apply: pc. have ws1:inc w (source (Vg (isf S) (J i j))) by rewrite sij - sui. have pc':sub (Vg M i) (source (Vg (isf S) (J i j))) by ue. have ws2: inc (Vf (Vg (isf S) (J i j)) w) (Vg M j). apply:qd'; apply/(Vf_image_P fij pc'); ex_tac. move:(f_equal (Vf^~w) hd'); rewrite ! compfV //; move ->. apply/(Vf_image_P fuj pb); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)