proposition: Lemma ex8_inl_subfm_hyp (S'' := inl_system_product same_I): inl_subfam_hyp S'' (Lg (isI S) (fun i => graph (Vg u i))).
proof: Proof. move:(inl_system_product_prop same_I); rewrite -/S'' => -[ha hb hc hd]. have pr1 j: inc j (isI S) -> sub (graph (Vg u j)) (Vg (isE S) j \times Vg (isE S') j). move => iI. by move: Hu=> [_ _ hu _];move: (hu _ iI) => [[[ _ qa] _ _ ] <- <-]. rewrite /inl_subfam_hyp; split; aww. rewrite hb ha; move => i iI; rewrite /inl_product_E !LgV//; exact:pr1. rewrite hc hd. move => i j lij t. move: (inl_prop0 lij) => [iI jI]. rewrite /inl_product_f !LgV//. move: (Hu) =>[ _ _ _ h]; move:(h _ _ lij) => cc {h}. move: (inl_prop4 lij) => [fij sij tij]. rewrite same_I in lij. move: (inl_prop4 lij) => [fij' sij' tij']. set f := _ \ftimes _. have ff: function f by apply: ext_to_prod_f. have sf: source f = (Vg (isE S) i \times Vg (isE S') i). by rewrite /f/ext_to_prod; aw; rewrite sij sij'; aw. have pr2: sub (graph (Vg u i)) (source f) by rewrite sf; exact: pr1. move/(Vf_image_P ff pr2) => [w wg ->]. rewrite /f ext_to_prod_V2 //;last by rewrite sij sij' - sf; apply: pr2. move: Hu=> [_ _ hu _];move: (hu _ jI) => [fuj suj tuj]. move: (hu _ iI) => [fui sui tui]. move: (Vf_pr2 fui wg) (p1graph_source1 fui wg) => qv pws. have pws': inc (P w) (Vg (isE S) i). rewrite - sui; exact: (p1graph_source1 fui wg). set x := (Vf (Vg (isf S) (J i j)) (P w)). have xsj: inc x (source (Vg u j)) by rewrite suj /x - tij; Wtac. move: (Vf_pr3 fuj xsj). have -> //: (Vf (Vg u j) x) = (Vf (Vg (isf S') (J i j)) (Q w)). have co1: Vg (isf S') (J i j) \coP Vg u i by split => //;rewrite sij'. have co2: Vg u j \coP Vg (isf S) (J i j) by split => //; ue. rewrite /x qv. move/(f_equal (Vf ^~(P w))):cc; rewrite ! compfV//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)