proposition: Lemma restr_axioms : forall f x, Function.axioms f -> Function.axioms (restr f x).
proof: Proof. ir. uhg; dj. rwi restr_inc_rw H0. uh H; ee. ap H; am. uh H; ee. ap H4. rwi restr_inc_rw H1; xd. rwi restr_inc_rw H2; xd. am. Qed.
imports: set_theory