proposition: Lemma gpaco4_gupaco clo r rg: gupaco4 clo (gpaco4 clo r rg) <4= gpaco4 clo r rg.
proof: Proof. eapply gpaco4_cofix. intros. destruct PR. econstructor. apply rclo4_rclo. eapply rclo4_mon. apply IN. intros. destruct PR. - apply rclo4_base. left. eapply paco4_mon. apply H. intros. left; apply CIH. econstructor. apply rclo4_base. right. destruct PR; apply H0. - destruct H. eapply rclo4_mon. apply IN0. intros. destruct PR; [| right; apply H]. left. eapply paco4_mon. apply H. intros. destruct PR. + left. apply INC. apply H0. + right. apply H0. Qed.
imports: Program.Basics Paco(paco4 pacotac)