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