proposition: Lemma Diffble_wd : forall F H, Feq I F H -> Diffble I pI F -> Diffble I pI H.
proof: Proof. intros F H H0 H1. elim H0; intros incF H2. elim H2; intros incH eqFH. inversion_clear H1. split; auto. intros; apply Diffble_I_wd with F; auto. apply included_Feq with I; auto. Qed.
imports: CoRN.ftc.MoreIntervals