proposition: Lemma conv_fun_seq'_wd_IR : conv_fun_seq'_IR _ _ _ contf contF -> conv_fun_seq'_IR _ _ _ contf0 contF0.
proof: Proof. intro H. red in |- *; intros. eapply conv_fun_seq'_wd. apply (H a b Hab Hinc). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions