proposition: Lemma gpaco1_gupaco clo r rg: gupaco1 clo (gpaco1 clo r rg) <1= gpaco1 clo r rg.
proof: Proof. eapply gpaco1_cofix. intros. destruct PR. econstructor. apply rclo1_rclo. eapply rclo1_mon. apply IN. intros. destruct PR. - apply rclo1_base. left. eapply paco1_mon. apply H. intros. left; apply CIH. econstructor. apply rclo1_base. right. destruct PR; apply H0. - destruct H. eapply rclo1_mon. apply IN0. intros. destruct PR; [| right; apply H]. left. eapply paco1_mon. apply H. intros. destruct PR. + left. apply INC. apply H0. + right. apply H0. Qed.
imports: Program.Basics Paco(paco1 pacotac)