proposition: Lemma noid_prop3 : projective_limit(noid_proj_system) = noid_projlim.
proof: Proof. move:(noid_prop1) => [Ha Hb Hc Hd He]. have dd: domain E = domain noid_E by rewrite /noid_E Lgd. set_extens t. move/prl_limitP => /= [ta tb tc td]; apply /Zo_P; split. apply/setXb_P; split => //. by rewrite tb . by move => i; rewrite domain_E => iI; apply:(noid_prop0 iI); apply: tc. move => // i j lij. have xM: inc (Vg t j) (Vg noid_E j). by apply: tc; rewrite - substrate_r; order_tac. by move: (td _ _ lij); rewrite (Hb _ _ _ lij xM). move =>/Zo_P [ /setXb_P [ta tb tc] td]. have Hf i: inc i I -> inc (Vg t i) (Vg noid_E i). move => iI; rewrite /noid_E LgV//. have ii: inc (J i i) r by apply: (proj32 preorder_r i); rewrite substrate_r. rewrite (td _ _ ii). case: (function_f ii); aw => [ff sf tf]. apply/(Imf_P ff); exists (Vg t i) => //; rewrite sf; apply: tc;ue. apply/prl_limitP => /=; split => //; first ue. move => i j lij. rewrite (td _ _ lij)(Hb _ _ _ lij) //; apply: Hf. rewrite - substrate_r; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)