proposition: Lemma inl_dl_fh_cp p (h := inl_can_fun inl_dl_systemS' (Q p)) (g:= inl_dl_fg (P p) (Q p)): inc p (isI S) -> h \coP g /\ function_prop (h \co g) (Vg (isE S) p) (inductive_limit (inl_dl_systemS')).
proof: Proof. rewrite inl_dl_I => /setX_P [pp Hi Hl]. move: (inl_dl_fg_fp Hi Hl) => [fg sg tg]. move: (inl_can_fun_fp (Hl:inc (Q p) (isI inl_dl_systemS'))) => [fh sh th]. have hh: source h = target g. by rewrite sh tg /= ! LgV//; apply: inl_dl_F_lambda_prop. rewrite pp in sg. split; saw; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)