proposition: Lemma prespect1_compatible' clo (RES: prespectful1 clo): compatible'1 (fun r => upaco1 gf (r \1/ clo r)).
proof: Proof. econstructor. { red; intros. eapply upaco1_mon. apply IN. intros. destruct PR. - left. apply LE, H. - right. eapply RES. apply H. intros. apply LE, PR. } intros r. assert (LEM: (gf'1 r \1/ clo (gf'1 r)) <1= (r \1/ clo r)). { intros. destruct PR. - left. apply H. - right. eapply RES. apply H. intros. apply PR. } intros. destruct PR. - split. + left. eapply paco1_mon. apply H. apply LEM. + apply paco1_unfold; [apply gf_mon|]. eapply paco1_mon. apply H. apply LEM. - split. + right. apply LEM. apply H. + destruct H. * eapply gf_mon. apply H. intros. right. left. apply PR. * apply paco1_unfold; [apply gf_mon|]. eapply RES, H; intros; apply PR. Qed.
imports: Program.Basics Paco(paco1 pacotac)