proposition: Lemma function_sub_V : forall f g x:E, Function.axioms g -> defined f x -> sub f g -> V x f = V x g.
proof: Proof. ir. cp H0; uh H0; ee. cp (Function.defined_lem H0 H2). cp (H1 _ H4). cp (Function.lem1 H H5). rwi pr1_pair H6. transitivity (pr2 (pair x (V x f))). rw pr2_pair; tv. rw H6. rw pr2_pair; tv. Qed.
imports: set_theory