proposition: Lemma inl_limit_nonempty S: (exists2 i, inc i (isI S) & nonempty (Vg (isE S) i)) <-> nonempty (inductive_limit S).
proof: Proof. split. move => [i iI [x xe]]; move: (inl_class_in_lim iI xe) => cs; ex_tac. move => [x /inductive_limit_hi [ha hb _]]; ex_tac; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)