proposition: Lemma gpaco3_gupaco clo r rg: gupaco3 clo (gpaco3 clo r rg) <3= gpaco3 clo r rg.
proof: Proof. eapply gpaco3_cofix. intros. destruct PR. econstructor. apply rclo3_rclo. eapply rclo3_mon. apply IN. intros. destruct PR. - apply rclo3_base. left. eapply paco3_mon. apply H. intros. left; apply CIH. econstructor. apply rclo3_base. right. destruct PR; apply H0. - destruct H. eapply rclo3_mon. apply IN0. intros. destruct PR; [| right; apply H]. left. eapply paco3_mon. apply H. intros. destruct PR. + left. apply INC. apply H0. + right. apply H0. Qed.
imports: Program.Basics Paco(paco3 pacotac)