proposition: Lemma ext2_pr2 g E E' z: (bijection_prop g E E') -> inc z (\Po (\Po E)) -> extension_p3 g z = Vf (extension_p2 g) z.
proof: Proof. by move => [[[ha _] _] hb] hc; apply:ext2_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)