proposition: Lemma Dprodi_continuous : forall (D:cpo)(I:Type)(Di:I->cpo) (f:D -m> Dprodi Di), (forall i, continuous (Proj Di i @ f)) -> continuous f.
proof: Proof. red; intros; intro i. apply Ole_trans with (lub (c:=Di i) ((Proj Di i @ f) @ h)); auto. exact (H i h). Qed.