proposition: Lemma lub_cont2_comp2_eq : forall (D1 D2 D3:cpo) (F : D1 -m> D2 -M-> D3), continuous2 F -> forall (f : natO-m>D1) (g :natO-m>D2), F (lub f) (lub g) == lub ((F@2 f) g).
proof: Proof. intros; apply lub_comp2_eq; auto. intro; apply (continuous2_app H). Qed.