proposition: Lemma inl_can_fun_ax S i : inc i (isI S) -> lf_axiom (fun x => class (inl_equiv S) (J x i)) (Vg (isE S) i) (inductive_limit S).
proof: Proof. move => iI x xE; apply: inc_class_setQ. rewrite inl_equiv_sr; apply/inl_sumP;aw; split ; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)