proposition: Lemma fcont_continuous2 : forall (D1 D2 D3:cpo) (f:D1-c>(D2-C->D3)), continuous2 (Fcontit D2 D3 @ fcontit f).
proof: Proof. intros; apply continuous_continuous2; intros. change (continuous (fcontit (f k))); auto. apply (continuous_comp (D1:=D1) (D2:=D2-C->D3) (D3:=D2-M->D3) (f:=Fcontit D2 D3)); auto. Qed.