proposition: Lemma partialApplyEq : forall {R : ConstructiveReals} (X : Set) (f g : @PartialFunction R X) (x : X) (xD : Domain f x) (xG : Domain g x), f = g -> (partialApply f x xD == partialApply g x xG).
proof: Proof. intros. subst g. apply DomainProp. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions