proposition: Lemma ext2_pr1 g E z: function g -> source g = E -> inc z (\Po (\Po E)) -> extension_p3 g z = Vf (extension_p2 g) z.
proof: Proof. move => ha hb /setP_P zi. by rewrite (etp_V (proj31 (etp_f (proj31 ha)))) // lf_source hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)