proposition: Lemma fixp_continuous_eq : forall (D:cpo) (h : natO -m> (D -M-> D)), (forall n, continuous (h n)) -> fixp (lub h) == lub (Fixp D @ h).
proof: Proof. intros; apply Ole_antisym; auto. exact (lub_comp_le (D1:=D -M-> D) (Fixp D) h). Qed.