proposition: Lemma gpaco0_cofix clo r rg l (OBG: forall rr (INC: rg <0= rr) (CIH: l <0= rr), l <0= gpaco0 clo r rr): l <0= gpaco0 clo r rg.
proof: Proof. assert (IN: l <0= gpaco0 clo r (rg \0/ l)). { intros. apply OBG; [left; apply PR0 | right; apply PR0 | apply PR]. } clear OBG. intros. apply IN in PR. destruct PR. econstructor. eapply rclo0_mon. apply IN0. clear IN0. intros. destruct PR; [|right; apply H]. left. revert H. pcofix CIH. intros. _punfold H0; [..|apply gpaco0_def_mon]. pstep. eapply gf_mon. apply H0. intros. apply rclo0_rclo. eapply rclo0_mon. apply PR. intros. destruct PR0. - apply rclo0_base. right. apply CIH. apply H. - destruct H; [destruct H|]. + apply rclo0_base. right. apply CIH0. left. apply H. + apply IN in H. destruct H. eapply rclo0_mon. apply IN0. intros. destruct PR0. * right. apply CIH. apply H. * right. apply CIH0. right. apply H. + apply rclo0_base. right. apply CIH0. right. apply H. Qed.
imports: Program.Basics Paco(paco0 pacotac)