proposition: Lemma map_wd_unfolded : forall (f : Homomorphism) (x y : R1), x[=]y -> f x[=]f y.
proof: Proof. intros. apply not_ap_imp_eq. intro H0. cut (Not (x[#]y)). intro H1. apply H1. apply map_strext_unfolded with (f := f). exact H0. apply eq_imp_not_ap. exact H. Qed.
imports: CoRN.reals.CReals