proposition: Lemma continuous2_comp2 : forall (D1 D2 D3 D4:cpo) (f:D3-m>D4)(g:D1-m>D2-M->D3), continuous f -> continuous2 g -> continuous2 (fcomp2 D1 D2 D3 D4 f g).
proof: Proof. red; intros. rewrite fcomp2_simpl. apply Ole_trans with (f (lub ((g@2 f0) g0))); auto. apply Ole_trans with (lub (f@((g@2 f0) g0))); auto. Qed.