proposition: Lemma DMAPi : forall (I:Type)(Di Dj:I->cpo)(f:forall i, Di i -c> Dj i), Dprodi Di -c> Dprodi Dj.
proof: Proof. intros; exists (Dmapi (fun i => fcontit (f i))). red; intros; intro i; rewrite Dmapi_simpl. repeat (rewrite Dprodi_lub_simpl). apply Ole_trans with (lub (c:=Dj i) (Fcontit (Di i) (Dj i) (f i) @ (Proj (fun x : I => Di x) i @ h))); auto. Defined.