proposition: Lemma ex8limit_graphs_prop t (i := (Q (rep (P t)))) (x := (P (rep (P t)))): inc t ex8_graphs_limit -> [/\ inc i (isI S), inc x (Vg (isE S) i) & t = J (class (inl_equiv S) (J x i)) (class (inl_equiv S') (J (Vf (Vg u i) x) i))].
proof: Proof. move: (inl_map2_prop same_I Hu). rewrite /ex8_graphs_limit; set f := inductive_limit_fun _ _ _. move => [[ff sf tf] _] tgf. rewrite -(function_sgraph ff tgf). move:(p1graph_source1 ff tgf) (Vf_pr2 ff tgf). rewrite sf => /inductive_limit_hi [iI xE ->] ->. have iI' : inc i (isI S') by rewrite - (inl_same_index_same_I same_I). by rewrite (inl_map_val_aux2 same_I Hu iI xE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)