Lemma iter_isdcpomorphism' (D : dcpowithbottom) : ∏ (n : nat), isdcpomorphism' (@iter D n). Proof. intros n I F isdirec g islubg. induction n as [| m IH]. - split. + intro i. simpl. apply dcpowithbottom_isMinimal. + intros y ineqs. apply dcpowithbottom_isMinimal. - simpl. eapply doublelubdirected. + exact isdirec. + exact IH. + set (islub' := pointwiselub_islub F isdirec). set (eq := lubsareunique _ islubg islub'). rewrite eq; cbn. apply pointwiselub_islubpointwise. Qed.
Require Import UniMath.Foundations.All.