proposition: Lemma integral_wd : Feq (Compact Hab) F G -> Integral F contF [=] Integral G contG.
proof: Proof. intro H. apply not_ap_imp_eq. intro H0. elim (integral_strext H0). intros x H1 H2. elim H; intros H3 H4. inversion_clear H4. generalize (H2 (contin_imp_inc _ _ _ _ contF x H1) (contin_imp_inc _ _ _ _ contG x H1)). apply eq_imp_not_ap. auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)