proposition: Lemma inductive_limit_hi S x (i := (Q (rep x))) (y := P (rep x)): inc x (inductive_limit S) -> [/\ inc i (isI S), inc y (Vg (isE S) i) & x = class (inl_equiv S) (J y i)].
proof: Proof. case/inductive_limitP; rewrite inl_equiv_sr. by move => /inl_sumP [pp px qx ->]; rewrite pp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)