proposition: Lemma function_tack_on_axioms : forall f x y:E, Function.axioms f -> ~inc x (domain f) -> Function.axioms (tack_on f (pair x y)).
proof: Proof. ir. uhg; ee; ir. rwi tack_on_inc H1. nin H1. uh H; ee; au. rw H1. rw pr1_pair; rw pr2_pair; tv. rwi tack_on_inc H1; rwi tack_on_inc H2; nin H1; nin H2. uh H; ee; au. assert False. ap H0. rwi H2 H3. rwi pr1_pair H3. wr H3. ap Function.lem2; try am. elim H4. assert False. ap H0. rwi H1 H3; rwi pr1_pair H3. rw H3. ap Function.lem2; try am. elim H4. rw H2; am. Qed.
imports: set_theory