proposition: Lemma prl_subfam_prop1 S M (g := prl_subfam_fct S M): prl_subfam_hyp S M -> [/\ forall z, inc z (psr S) -> restriction2_axioms (Vg (psf S) z) (Vg M (Q z)) (Vg M (P z)), forall i j x, gle (psr S) i j -> inc x (Vg M j) -> Vf (Vg g (J i j)) x = Vf (Vg (psf S) (J i j)) x, forall i, inc i (psr S)-> function_prop (Vg g i) (Vg M (Q i)) (Vg M (P i)), forall i j k, gle (psr S) i j -> gle (psr S) j k -> Vg g (J i j) \co Vg g (J j k) = Vg g (J i k) & forall i, inc i (psI S) -> Vg g (J i i) = identity (Vg M i)].
proof: Proof. move =>[pa pb pc pd]. have rc z: inc z (psr S) -> restriction2_axioms (Vg (psf S) z) (Vg M (Q z)) (Vg M (P z)). move => zr. move:(ps_function_f zr) =>[ff sf tf]. move: (pr1_sr zr)(pr2_sr zr); rewrite ps_substrate_r => iI jI. split. - done. - by rewrite sf; apply: pc. - by rewrite tf; apply: pc. - have pz:= ((proj31 (ps_preorder_r S)) _ zr). by rewrite -{1} pz;apply: pd; rewrite/ gle/related pz. have rd:forall i j x, gle (psr S) i j -> inc x (Vg M j) -> Vf (Vg g (J i j)) x = Vf (Vg (psf S) (J i j)) x. move => i j x ha hb. have hb':inc x (Vg M (Q (J i j))) by aw. rewrite -(restriction2_V (rc _ ha) hb'); rewrite /g/prl_subfam_fct LgV//. have re i: inc i (psr S) -> function_prop (Vg g i) (Vg M (Q i)) (Vg M (P i)). move => ir; rewrite /g/prl_subfam_fct LgV//. exact: (restriction2_prop (rc _ ir)). have rg i: inc i (psI S) -> Vg g (J i i) = identity (Vg M i). move => ii. have iiI:= (prl_prop1 ii). move:(re _ iiI); aw => fp; apply: (identity_prop0 fp) => x xM. by rewrite (rd _ _ _ iiI xM) (ps_identity_f ii) LfV//; apply: pc. split => // i j k lij ljk. have lik: gle (psr S) i k by apply: (proj33 (ps_preorder_r S)) lij ljk. move: (re _ lij) => [fij sij tij]. move: (re _ ljk) => [fjk sjk tjk]. move: (re _ lik) => [fik sik tik]. rewrite ! pr1_pair in tij tik tjk. rewrite ! pr2_pair in sij sik sjk. have co1: Vg g (J i j) \coP Vg g (J j k) by split => //; rewrite sij tjk. have fc1: function (Vg g (J i j) \co Vg g (J j k)) by apply: compf_f. apply: function_exten => //. - by aw; rewrite sik sjk. - by aw; rewrite tij tik. aw; rewrite sjk => x xM. have cpp: Vg (psf S) (J i j) \coP Vg (psf S) (J j k). move: (ps_function_f lij) => [fa fb fc]. move: (ps_function_f ljk) => [fa' fb' fc']. by split => //; rewrite fb fc'; aw. have vm: inc (Vf (Vg g (J j k)) x) (Vg M j). by rewrite - tjk; apply:(Vf_target fjk); rewrite sjk. have xM': inc x (source (Vg (psf S) (J j k))). move: (ps_function_f ljk) => [_ -> _]; aw; apply:pc => //. rewrite - (ps_substrate_r); order_tac. have xM'': inc x (source (Vg g (J j k))) by rewrite sjk. rewrite (rd _ _ _ lik xM) - (ps_compose_f lij ljk). by rewrite !compfV //(rd _ _ _ lij vm) (rd _ _ _ ljk xM). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)