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 contF0.
proof: Proof. intros H H0 a b Hab Hinc. eapply conv_fun_seq'_wdl with (f := f). 2: apply (H0 a b Hab Hinc). intro; elim (H n); intros. inversion_clear b0. apply eq_imp_Feq; Included. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions