proposition: Lemma etp_identity x: \Pof (identity x) = identity (\Po x).
proof: Proof. have ic:=(@identity_corresp x). apply: function_exten; fprops. by rewrite/extension_to_parts; aw. by rewrite/extension_to_parts; aw. move=> y /=; rewrite {1} /extension_to_parts; aw => ys1. move /setP_P: (ys1) => ys2. have ys: sub y (source (identity x)) by aw; apply/setP_P. have fi: (function (identity x)) by fprops. rewrite etp_V // idV //; set_extens t. by move /(Vf_image_P fi ys)=> [u uy]; rewrite idV; [ move=> -> | apply: ys2]. by move => ty;apply /(Vf_image_P fi ys); ex_tac; rewrite idV //; apply: ys2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)