proposition: Lemma ex3_gl_val_ax: lf_axiom ex3_gl_val ex3_graphs_limit (projective_limit ex3limit_graphs).
proof: Proof. move => t. move:(prl_subsets_prop ex3_prl_subfm_hyp). rewrite -/ex3limit_graphs; move => [s_E s_I s_r s_f]. move: (prl_map2_prop same_I Hu). rewrite / ex3_graphs_limit; set f := projective_limit_fun _ _ _. move => [[ff sf tf] fp] tgf. move:(p1graph_source1 ff tgf) (p2graph_target1 ff tgf) (Vf_pr2 ff tgf). rewrite sf tf => ps qt xv. move: (Hu) => [hu1 hu2 hu3 hu4]. move/prl_limitP:(ps) => [pg pd pv pw]. apply/prl_limitP; rewrite s_E s_f /ex3_gl_val; split. - fprops. - by aw. - aw => i iI; rewrite ! LgV//. move: (hu3 _ iI) => [fu su tu]. have ha: inc (Vg (P t) i) (source (Vg u i)) by rewrite su; apply: pv. rewrite xv -(prl_map_val_aux2 same_I Hu iI ps). exact: (Vf_pr3 fu ha). - move:(prl_system_product_prop same_I) =>[s_E' s_I' s_r' s_f']. move: (prl_subfam_prop1 ex3_prl_subfm_hyp). rewrite s_r s_r'; set F := prl_subfam_fct _ _. move => [qa qb qc qd qe]. move => i j lij. move: (lij); rewrite same_I => lij'. move: (prl_prop0 lij) => [iI jI]. move:(ps_function_f lij) =>[fij sij tij]. move:(ps_function_f lij') =>[fij' sij' tij']. move/prl_limitP:(qt) => [qg q_d qv qw]. rewrite /ex3_gl_val LgV// LgV//. move: (qb i j (J (Vg (P t) j) (Vg (Q t) j)) lij); rewrite LgV// => hh. have ww: inc (J (Vg (P t) j) (Vg (Q t) j)) (source (Vg (psf S) (J i j)) \times source (Vg (psf S') (J i j))). rewrite /ext_to_prod; aw; rewrite sij sij'. apply:setXp_i; aw. - by apply:pv. - by apply:qv; rewrite - (prl_same_index_same_I same_I). have qq: inc (J (Vg (P t) j) (Vg (Q t) j)) (graph (Vg u j)). move:(hu3 _ jI) => [fu su tu]. rewrite xv - prl_map_val_aux2//; apply: (Vf_pr3 fu); rewrite su. by apply: pv. rewrite (hh qq) s_f' /prl_product_f (LgV lij)(ext_to_prod_V2 fij fij' ww). by rewrite pr1_pair pr2_pair -(pw _ _ lij) - (qw _ _ lij'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)