proposition: Lemma prespect12_compatible' clo (RES: prespectful12 clo): compatible'12 (fun r => upaco12 gf (r \12/ clo r)).
proof: Proof. econstructor. { red; intros. eapply upaco12_mon. apply IN. intros. destruct PR. - left. apply LE, H. - right. eapply RES. apply H. intros. apply LE, PR. } intros r. assert (LEM: (gf'12 r \12/ clo (gf'12 r)) <12= (r \12/ clo r)). { intros. destruct PR. - left. apply H. - right. eapply RES. apply H. intros. apply PR. } intros. destruct PR. - split. + left. eapply paco12_mon. apply H. apply LEM. + apply paco12_unfold; [apply gf_mon|]. eapply paco12_mon. apply H. apply LEM. - split. + right. apply LEM. apply H. + destruct H. * eapply gf_mon. apply H. intros. right. left. apply PR. * apply paco12_unfold; [apply gf_mon|]. eapply RES, H; intros; apply PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)