proposition: Lemma lift_eq_complete_2 : forall (A B C: MetricSpace) (f g : Complete A --> Complete B --> C), (forall a b, msp_eq (f (Cunit a) (Cunit b)) (g (Cunit a) (Cunit b))) -> (forall a b, msp_eq (f a b) (g a b)).
proof: Proof. intros A B C f g H a. apply lift_eq_complete. intro b. revert a. assert (@is_UniformlyContinuousFunction (Complete A) C (fun a => f a (Cunit b)) (mu f)). { intros e x y H0. apply (uc_prf f e x y H0). } assert (@is_UniformlyContinuousFunction (Complete A) C (fun a => g a (Cunit b)) (mu g)). { intros e x y H1. apply (uc_prf g e x y H1). } apply (@lift_eq_complete A C (Build_UniformlyContinuousFunction H0) (Build_UniformlyContinuousFunction H1)). simpl. intro a. apply H. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax