proposition: Lemma prl_direct_hyp S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> prl_subfam_hyp S' (prl_dirim_set u).
proof: Proof. move => pss [pa pb pc pd]. have ssI := (prl_same_index_same_I pss). rewrite /prl_dirim_set; split. - fprops. - by aw; rewrite pb ssI. - move => i; rewrite - ssI => iI. have idu: inc i (domain u) by rewrite pb. move:(pc _ iI) =>[fu su tu]. by rewrite LgV // - tu; apply:Imf_Starget. rewrite - pss pb;move => i j lij. have lij':gle (psr S') i j by rewrite - pss. move:(ps_function_f lij); aw => - [fij sij tij]. move:(ps_function_f lij'); aw => - [fij' sij' tij']. move:(prl_prop0 lij)=> [iI jI]. move:(pc _ iI) =>[fui sui tui]. move:(pc _ jI) =>[fuj suj tuj]. have ss1: (sub (Imf (Vg u j)) (source (Vg (psf S') (J i j)))). by rewrite sij' - tuj;apply:Imf_Starget. have hb: Vg u i \coP Vg (psf S) (J i j). by split => //; rewrite sui tij; aw. have hc: Vg (psf S') (J i j) \coP Vg u j. by split => //; rewrite sij' tuj. move => t; rewrite ! LgV//. move /(Vf_image_P fij' ss1) => [x /(Imf_P fuj) [y ya ->] ->]. have ysv: inc y (source (Vg (psf S) (J i j))) by rewrite sij - suj. move:(f_equal (Vf ^~y) (pd _ _ lij)); rewrite ! compfV//; move <-. have hhh: inc (Vf (Vg (psf S) (J i j)) y) (source (Vg u i)). rewrite sui -tij; Wtac. apply/(Imf_P fui); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)