proposition: Lemma conv_fun_seq'_wdr'_IR : Feq J F G -> conv_fun_seq'_IR _ _ _ contf contF -> conv_fun_seq'_IR _ _ _ contf contG.
proof: Proof. intros H H0 a b Hab Hinc. eapply conv_fun_seq'_wdr' with (F := F). 2: apply (H0 a b Hab Hinc). apply included_Feq with J; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions