proposition: Lemma function_sub_eq : forall r s, Function.axioms r -> Function.axioms s -> sub r s -> sub (domain s) (domain r) -> r = s.
proof: Proof. ir. ap extensionality; try am. uhg; ir. cp (Function.lem1 H0 H3). cp (Function.lem2 H0 H3). assert (inc (pr1 x) (domain r)). ap H2; am. util (Function.defined_lem (f:=r) (x:=(pr1 x))). am. uhg; ee; am. assert (inc (pair (pr1 x) (V (pr1 x) r)) s). ap H1; am. rwi H4 H3. uh H0; ee. assert (pair (pr1 x) (V (pr1 x) r) = pair (pr1 x) (V (pr1 x) s)). ap H9. am. am. do 2 (rw pr1_pair). tv. rwi H10 H7. wri H4 H7. am. Qed.
imports: set_theory