fact: Definition PartialRestriction {R : ConstructiveReals} {X : Set} (f g : @PartialFunction R X) : Type := prod (DomainInclusion f g) (forall (x : X) (xD : Domain f x) (xG : Domain g x), partialApply f x xD == partialApply g x xG).
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete