proposition: Lemma ex8_gl_val_bf (E := (inductive_limit ex8limit_graphs)) (f:= Lf ex8_gl_val ex8_graphs_limit E): bijection_prop f ex8_graphs_limit E.
proof: Proof. have ax:= ex8_gl_val_ax. rewrite /f;saw. case:(inl_map2_prop same_I Hu); set fp := (inductive_limit_fun S S' u). move => [fff sff tff] ffp. move:(inl_subfam_prop1 ex8_inl_subfm_hyp). set g := inl_subfam_fct _ _; set S'':= (inl_system_product same_I). move => [gp1 gp2 gp3 gp4 gp5]. have Ha i k x : gle (isr S) i k -> inc x (Vg (isE S) i) -> Vf (Vg (isf S'') (J i k)) (J x (Vf (Vg u i) x)) = J (Vf (Vg (isf S) (J i k)) x) (Vf (Vg (isf S') (J i k)) (Vf (Vg u i) x)). move => ha hb;rewrite /= /(inl_product_f); rewrite LgV//. move:(inl_prop4 ha) =>[fa sa ta]. have xs1:inc x (source (Vg (isf S) (J i k))) by ue. move:(proj1(inl_prop0 ha)) => iI. rewrite same_I in ha. move:(inl_prop4 ha) =>[fa' sa' ta']. have xs2: inc (Vf (Vg u i) x) (source (Vg (isf S') (J i k))). move: (proj43 Hu _ iI) => [fui sui tui]; rewrite sa'; Wtac. by rewrite ext_to_prod_V. apply: (lf_bijective ax). move => t t' /ex8limit_graphs_prop []. set i := Q _; set x := P _ => iI xE eq1. move => /ex8limit_graphs_prop []. set i' := Q _; set x' := P _ => iI' xE' eq2. rewrite /ex8_gl_val -/i -/i' -/x -/x'. move: (proj43 Hu _ iI) => [fui sui tui]. move: (proj43 Hu _ iI') => [fui' sui' tui']. have ha: inc (J x (Vf (Vg u i) x)) (Vg (Lg (isI S) (fun z => graph (Vg u z))) i). by rewrite LgV//; apply: Vf_pr3 => //; ue. have hb: inc (J x' (Vf (Vg u i') x')) (Vg (Lg (isI S) (fun z => graph (Vg u z))) i'). by rewrite LgV//; apply: Vf_pr3 => //; ue. move/(inl_class_eq_bis) => /= ww; move: (ww iI iI' ha hb). move => [k []]; aw; simpl. move => lik lik'. rewrite -/g gp2 // gp2 // Ha // Ha // => eq3. move:(pr1_def eq3) (pr2_def eq3) => eq4 eq5. rewrite eq1 eq2; congr J. by rewrite -(inl_class_of_fij lik xE) eq4 (inl_class_of_fij lik' xE'). have hc: inc (Vf (Vg u i) x) (Vg (isE S') i) by Wtac. have hd:inc (Vf (Vg u i') x') (Vg (isE S') i') by Wtac. rewrite same_I in lik lik'. by rewrite -(inl_class_of_fij lik hc) eq5 - (inl_class_of_fij lik' hd). move => y /inductive_limit_hi; set i := Q _ ; set x := P _; simpl. move => [iI]; rewrite !LgV// => yg ->. move: (proj43 Hu _ iI) => [fui sui tui]. move:(in_graph_Vf fui yg) => xv. move:(p1graph_source1 fui yg) (p2graph_target1 fui yg);rewrite sui tui=> xE XE'. set c1 := class (inl_equiv S) (J (P x) i). have c1l: inc c1 (inductive_limit S). by apply: inl_class_in_lim. set c2 := class (inl_equiv S') (J (Vf (Vg u i) (P x)) i). have c2v: c2 = Vf fp c1 by rewrite inl_map_val_aux2. have zl:inc (J c1 c2) ex8_graphs_limit. rewrite /ex8_graphs_limit c2v; apply: Vf_pr3 => //; ue. ex_tac. move/inductive_limit_hi:c1l; set j := Q (rep c1); set z := P (rep c1); move => [jI zE qc]. rewrite /ex8_gl_val; aw; rewrite -/j -/z. move: (proj43 Hu _ jI) => [fuj suj tuj]. have ha: inc (J z (Vf (Vg u j) z)) (graph (Vg u j)). by apply: Vf_pr3 => //; ue. have hb: inc (J (P x) (Vf (Vg u i) (P x))) (graph (Vg u i)) by rewrite - xv. apply/inl_class_eq_bis=> //. simpl; rewrite LgV//. by simpl; rewrite LgV//; apply: Vf_pr3 => //; ue. move: qc; rewrite /c1. move/(inl_class_eq_bis iI jI xE zE) => [k []]; aw => lik ljk sv. exists k; saw. rewrite xv; rewrite gp2 //; last by rewrite LgV. rewrite gp2 //; last by rewrite LgV. rewrite Ha // Ha//. rewrite (inl_map2_compat_prop0 same_I Hu xE lik). by rewrite (inl_map2_compat_prop0 same_I Hu zE ljk) sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)