proposition: Lemma inl_subfam_prop1 S M (g := inl_subfam_fct S M): inl_subfam_hyp S M -> [/\ forall z, inc z (isr S) -> restriction2_axioms (Vg (isf S) z) (Vg M (P z)) (Vg M (Q z)), forall i j x, gle (isr S) i j -> inc x (Vg M i) -> Vf (Vg g (J i j)) x = Vf (Vg (isf S) (J i j)) x, forall i, inc i (isr S)-> function_prop (Vg g i) (Vg M (P i)) (Vg M (Q i)), forall i j k, gle (isr S) i j -> gle (isr S) j k -> Vg g (J j k) \co Vg g (J i j) = Vg g (J i k) & forall i, inc i (isI S) -> Vg g (J i i) = identity (Vg M i)].
proof: Proof. move =>[pa pb pc pd]. have rc z: inc z (isr S) -> restriction2_axioms (Vg (isf S) z) (Vg M (P z)) (Vg M (Q z)). move => zr. move:(is_function_f zr) =>[ff sf tf]. move: (pr1_sr zr)(pr2_sr zr) => iI jI. split. - done. - by rewrite sf; apply: pc; rewrite -is_substrate_r. - by rewrite tf; apply: pc;rewrite -is_substrate_r. - have pz:= ((proj31 (is_preorder_r S)) _ zr). by rewrite -{1} pz;apply: pd; rewrite/ gle/related pz. have rd:forall i j x, gle (isr S) i j -> inc x (Vg M i) -> Vf (Vg g (J i j)) x = Vf (Vg (isf S) (J i j)) x. move => i j x ha hb. have hb':inc x (Vg M (P (J i j))) by aw. rewrite -(restriction2_V (rc _ ha) hb'); rewrite /g/inl_subfam_fct LgV//. have re i: inc i (isr S) -> function_prop (Vg g i) (Vg M (P i)) (Vg M (Q i)). move => ir; rewrite /g/inl_subfam_fct LgV//. exact: (restriction2_prop (rc _ ir)). have rg i: inc i (isI S) -> Vg g (J i i) = identity (Vg M i). move => ii. have iiI: inc (J i i) (isr S) by apply: inl_prop1. move:(re _ iiI); aw => fh;apply:(identity_prop0 fh) => x xM. by rewrite (rd _ _ _ iiI xM) (is_identity_f ii) idV//; apply: pc. split => // i j k lij ljk. have lik: gle (isr S) i k by apply: (proj33 (is_preorder_r S)) lij ljk. move: (re _ lij) => [fij sij tij]. move: (re _ ljk) => [fjk sjk tjk]. move: (re _ lik) => [fik sik tik]. rewrite ! pr2_pair in tij tik tjk. rewrite ! pr1_pair in sij sik sjk. have co1: Vg g (J j k) \coP Vg g (J i j) by split => //; ue. have fc1: function (Vg g (J j k) \co Vg g (J i j)) by apply: compf_f. apply: function_exten => //. - by aw; ue. - by aw; ue. aw; rewrite sij => x xM. have ha: inc x (Vg (isE S) i) by apply: (pc _ (proj1 (inl_prop0 lij))). have hb: inc x (source (Vg g (J i j))) by ue. move:(inl_prop4 lij) => [fa ffb fc]. have : inc (Vf (Vg g (J i j)) x) (Vg M j). rewrite - tij; Wtac. rewrite (rd _ _ _ lij xM) => hd. have hc: inc x (source (Vg (isf S) (J i j))) by ue. by rewrite compfV // !rd // inl_prop3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)