proposition: Lemma etp_compose: {when: composableC, {morph extension_to_parts: x y / x \co y }}.
proof: Proof. move=> g f /= cgf; symmetry. have cegf:= (etp_composable cgf). have [cf cg cfg] := cgf. have ccg: (correspondence (g \co f)) by apply: compf_correspondence. apply: function_exten; try fct_tac; fprops; try solve[rewrite /extension_to_parts ; aw; trivial]. aw; move => x xs. move: (xs). rewrite lf_source => /setP_P xs1. have xs2: sub x (source (g \co f)) by aw. rewrite compfV // ! etp_V //. by rewrite /compose/Vfs; aw; symmetry; apply:compg_image. rewrite cfg; apply: (@sub_trans (range (graph f))); fprops. apply: dirim_Sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)