proposition: Lemma ex9_propg (h: right_directed_on r I) (S := InductiveSystem or sr h fgE dE fgf df function_f compose_f identity_f): ex9_quo = inductive_limit S.
proof: Proof. move:(ex9_rels_special h) => eqxx. set_extens t. by move/ex9_quoP; rewrite eqxx => w; apply/inductive_limitP. by move/inductive_limitP => w;apply/ex9_quoP; rewrite eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)