proposition: Lemma fun_image_wd : Feq I F G -> forall x, fun_image F I x -> fun_image G I x.
proof: Proof. intros H x H0. elim H; clear H; intros H H1. elim H1; clear H1; intros H2 H3. elim H0; intros y Hy. exists y. elim Hy; intros H4 H1. elim H1; clear Hy H1; intros H5 H6. split; auto. split; auto. intro; Step_final (F y H5). Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1