proposition: Lemma conv_fun_seq_wd_IR : conv_fun_seq_IR _ _ contf -> conv_fun_seq_IR _ _ 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