proposition: Lemma ex8_gl_val_ax: lf_axiom ex8_gl_val ex8_graphs_limit (inductive_limit ex8limit_graphs).
proof: Proof. move => t / ex8limit_graphs_prop. rewrite /ex8_gl_val. set i := (Q (rep (P t))); set x := (P (rep (P t))). move => [iI xE _]; apply:inl_class_in_lim => //=; rewrite LgV//. move: (proj43 Hu _ iI) => [fui sui tui];apply: Vf_pr3 => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)