proposition: Lemma noid_prop5b z: inc z r -> restriction2_axioms (Vg f z) (Vg noid_E' (P z)) (Vg noid_E' (Q z)).
proof: Proof. move => zr. move:(function_f zr) =>[ff sf tf]. move: (pr1_sr zr)(pr2_sr zr); rewrite substrate_r => iI jI. move:(noid_prop5a iI); rewrite /noid_E' LgV// - sf => hu. split. - done. - done. - rewrite tf; move:(noid_prop5a jI); rewrite /noid_E' LgV//. - have pz:= ((proj31 preorder_r) _ zr). move => t /(Vf_image_P ff hu) [u uif ->]. move:(zr); rewrite - pz => zr'. have ii: inc (J (P z) (P z)) r by apply: (proj32 preorder_r (P z)); rewrite substrate_r. have jj: inc (J(Q z) (Q z)) r by apply: (proj32 preorder_r (Q z)); rewrite substrate_r. case:(function_f ii); aw => fii sii tii. case:(function_f jj); aw => fjj sjj tjj. have co1: Vg f z \coP Vg f (J (P z) (P z)) by split => //; ue. have co2: Vg f (J (Q z) (Q z)) \coP Vg f z by split => //; ue. move/(Imf_P fii):uif => [v]; rewrite sii => vej vv. rewrite LgV//; apply/(Imf_P fjj); rewrite sjj vv. exists (Vf (Vg f z) v); first Wtac. move:(compose_f ii zr') (compose_f zr' jj); aw; rewrite pz => eqa eqb. move:(f_equal (Vf ^~ v) eqa)(f_equal (Vf ^~ v) eqb). rewrite !compfV //;try ue; move => -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)