proposition: Lemma etp_fun A B f: inc f (functions A B) -> inc (\Pof f) (functions (\Po A) (\Po B)).
proof: Proof. move/functionsP => [ff st tf]; apply /functionsP; split. - by apply: etp_f; case ff. - by rewrite /extension_to_parts - st; aw. - by rewrite /extension_to_parts - tf; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)