proposition: Lemma prespect8_compatible' clo (RES: prespectful8 clo): compatible'8 (fun r => upaco8 gf (r \8/ clo r)).
proof: Proof. econstructor. { red; intros. eapply upaco8_mon. apply IN. intros. destruct PR. - left. apply LE, H. - right. eapply RES. apply H. intros. apply LE, PR. } intros r. assert (LEM: (gf'8 r \8/ clo (gf'8 r)) <8= (r \8/ clo r)). { intros. destruct PR. - left. apply H. - right. eapply RES. apply H. intros. apply PR. } intros. destruct PR. - split. + left. eapply paco8_mon. apply H. apply LEM. + apply paco8_unfold; [apply gf_mon|]. eapply paco8_mon. apply H. apply LEM. - split. + right. apply LEM. apply H. + destruct H. * eapply gf_mon. apply H. intros. right. left. apply PR. * apply paco8_unfold; [apply gf_mon|]. eapply RES, H; intros; apply PR. Qed.
imports: Program.Basics Paco(paco8 pacotac)