proposition: Lemma conv_fun_seq'_wdl'_IR : (forall n, Feq J (f n) (g n)) -> conv_fun_seq'_IR _ _ _ contf contF -> conv_fun_seq'_IR _ _ _ contg contF.
proof: Proof. intros H H0 a b Hab Hinc. eapply conv_fun_seq'_wdl' with (f := f); auto. intro; elim (H n); intros. inversion_clear b0. apply eq_imp_Feq; Included. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions