On Partial functions

Consider the following module:
Require Import Ensembles.

Set Implicit Arguments.

(** A partial function is characterized by a domain, a codomain,
  and a total function *)

Record partial_function (A B : Type) : Type := {
  domain : Ensemble A ;
  codomain : Ensemble B;
  ap : A -> B;
  domain_ok : forall a, In _ domain a -> In _ codomain (ap a)}.

(** Equality on partial functions *)
 
Inductive pfun_eq (A B : Type)(F G : partial_function A B) :
 Prop :=
 mk_pfun_eq : domain F = domain G ->
              codomain F = codomain G ->
              (forall a, In _ (domain F) a ->
                         ap F a = ap G a) ->
              pfun_eq F G.


(** equality on partial functions is Leibniz equality  *)

Axiom pfun_extensionality : forall (A B : Type)
                                   (F G : partial_function A B),
                                    pfun_eq F G -> F = G.

Is it a good formalization of partial functions?

Solution

Look at this file .
Going home