proposition: Lemma ex6_F_prop1 x (j := Q (rep x)) (i := (Q (rep (P (rep x))))) (y := P (rep (P (rep x)))): inc x (inductive_limit ex6_F) -> [/\ inc j L, inc i (Vg Jf j), inc y (Vg (isE S) i) & x = ex6_F_val y i j].
proof: Proof. move/inductive_limit_hi => []; simpl; rewrite /ex6_F_val -/j => jL h xv. move:h; rewrite LgV//; rewrite (ex6_res0 jL) (ex6_prop6a jL). by move/inductive_limit_hi; rewrite /= -/i -/y; move => [ha]; rewrite LgV// => hb <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)