proposition: Lemma Derivative_unique : Derivative I pI F G -> Derivative I pI F H -> Feq I G H.
proof: Proof. intros H0 H1. elim H0; intros incF H0'. elim H0'; intros incG derFG. elim H1; intros incF' H1'. elim H1'; intros incH derFH. apply included_Feq''; intros. auto. unfold Hab'; apply Derivative_I_unique with F; Deriv. Qed.
imports: CoRN.ftc.MoreIntervals