proposition: Lemma FIXP_proj : forall (I:Type)(DI: I -> cpo) (F:Dprodi DI -c>Dprodi DI) (i:I) (fi : DI i -c> DI i), (forall X : Dprodi DI, F X i == fi (X i)) -> FIXP (Dprodi DI) F i == FIXP (DI i) fi.
proof: Proof. intros; apply Ole_antisym. rewrite FIXP_simpl. rewrite Fixp_simpl. unfold fixp. rewrite Dprodi_lub_simpl. apply lub_le . induction n; auto. rewrite fmon_comp_simpl. rewrite (iterS_simpl (fcontit F)). rewrite (Proj_simpl (O:=DI) i). apply Ole_trans with (fi (iter (D:=Dprodi DI) (fcontit F) n i)). case (H (iter (D:=Dprodi DI) (fcontit F) n)); trivial. apply Ole_trans with (fi (FIXP (DI i) fi)); auto. apply FIXP_inv. case (H (FIXP (Dprodi DI) F)); intros. apply Ole_trans with (1:=H1). case (FIXP_eq F); auto. Qed.