proposition: Lemma inl_class_in_lim S i x: inc i (isI S) -> inc x (Vg (isE S) i) -> inc (class (inl_equiv S) (J x i)) (inductive_limit S).
proof: Proof. move => iI xE; apply/inductive_limitP. have [ha hb]:=(inl_equiv_esr S). apply:(class_class ha); rewrite hb; apply/inl_sumP; aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)