proposition: Lemma continuous2_continuous : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3), continuous2 F -> continuous F.
proof: Proof. red; intros; intro k. apply Ole_trans with (F (lub h) (lub (mseq_cte k)) ); auto. apply Ole_trans with (lub ((F @2 h) (mseq_cte k))); auto. Qed.