proposition: Lemma ext2_pr3 E E' g z: bijection_prop g E E' -> inc z (\Po (\Po E)) -> forall t, (inc t (extension_p3 g z) <-> exists2 u, inc u z & t = (Vfs g u)).
proof: Proof. move => [pa pb pc] /setP_P zz t. have fg := (proj1 (proj1 pa)). have cg := (proj31 fg). have pe: sub z (source (extension_to_parts g)) by rewrite lf_source pb. split. move/(Vf_image_P (etp_f cg) pe) => [u ua ->]. have sug: sub u (source g) by rewrite pb; apply /setP_P; apply: zz. rewrite (etp_V cg sug); ex_tac. move => [u uz ->]. have sug: sub u (source g) by rewrite pb; apply /setP_P; apply: zz. rewrite - (etp_V cg sug); apply /(Vf_image_P (etp_f cg) pe); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)