proposition: Lemma inl_dl_fg_fp i l (Hi: inc i I1) (Hl: inc l I2): function_prop (inl_dl_fg i l) (Vg (isE S) (J i l)) (inductive_limit (inl_dl_S_lambda Hl)).
proof: Proof. move:(inl_can_fun_fp (Hi:inc i (isI (inl_dl_S_lambda Hl)))). rewrite inl_dl_fg_prop1 /=/inl_dl_Elam_fam LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)