proposition: Lemma comp_inc_lemma : forall F, maps_compacts_into_weak F -> forall x Hx, I x -> J (F x Hx).
proof: Proof. intros F H x Hx H0. cut (included (Compact (leEq_reflexive _ x)) I). intro H1. elim (H _ _ _ H1); intros c Hc. elim Hc; clear Hc; intros d Hd. elim Hd; clear Hd; intros Hcd Hmap'. elim Hmap'; intros H2 H3. apply H2; apply H3; auto. split; apply leEq_reflexive. intros x0 H1. inversion_clear H1. apply iprop_wd with x; auto. apply leEq_imp_eq; auto. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries