proposition: Lemma prespect7_compatible' clo (RES: prespectful7 clo): compatible'7 (fun r => upaco7 gf (r \7/ clo r)).
proof: Proof. econstructor. { red; intros. eapply upaco7_mon. apply IN. intros. destruct PR. - left. apply LE, H. - right. eapply RES. apply H. intros. apply LE, PR. } intros r. assert (LEM: (gf'7 r \7/ clo (gf'7 r)) <7= (r \7/ clo r)). { intros. destruct PR. - left. apply H. - right. eapply RES. apply H. intros. apply PR. } intros. destruct PR. - split. + left. eapply paco7_mon. apply H. apply LEM. + apply paco7_unfold; [apply gf_mon|]. eapply paco7_mon. apply H. apply LEM. - split. + right. apply LEM. apply H. + destruct H. * eapply gf_mon. apply H. intros. right. left. apply PR. * apply paco7_unfold; [apply gf_mon|]. eapply RES, H; intros; apply PR. Qed.
imports: Program.Basics Paco(paco7 pacotac)