proposition: Lemma fcont_Comp_continuous2 : forall (D1 D2 D3:cpo), continuous2 (fcont_Comp D1 D2 D3).
proof: Proof. red; intros. change ((lub f) @_ (lub g) <= lub (c:=D1 -C-> D3) ((fcont_Comp D1 D2 D3 @2 f) g)). apply fcont_le_intro; intro x; rewrite fcont_comp_simpl. repeat (rewrite fcont_lub_simpl). rewrite fcont_app_continuous. rewrite double_lub_diag. apply lub_le_compat; simpl; auto. Qed.