proposition: Lemma function_glueing : forall z, (forall f, inc f z -> Function.axioms f) -> (forall f g x, inc f z -> inc g z -> defined f x -> defined g x -> (V x f) = (V x g)) -> Function.axioms (union z).
proof: Proof. ir. uhg; ee; ir. nin (union_exists H1); ee. cp (H _ H3). uh H4. ee. ap H4; am. nin (union_exists H1); nin (union_exists H2); ee. cp (H _ H7); cp (H _ H6). cp (Function.lem1 H8 H4). cp (Function.lem1 H9 H5). rw H10; rw H11. rw H3. assert (V (pr1 y) x0 = V (pr1 y) x1). ap H0. am. am. uhg; ee; try am. wr H3; ap Function.lem2; try am. uhg; ee; try am; ap Function.lem2; try am. rw H12; tv. Qed.
imports: set_theory