proposition: Lemma gpaco5_cofix clo r rg l (OBG: forall rr (INC: rg <5= rr) (CIH: l <5= rr), l <5= gpaco5 clo r rr): l <5= gpaco5 clo r rg.
proof: Proof. assert (IN: l <5= gpaco5 clo r (rg \5/ l)). { intros. apply OBG; [left; apply PR0 | right; apply PR0 | apply PR]. } clear OBG. intros. apply IN in PR. destruct PR. econstructor. eapply rclo5_mon. apply IN0. clear x0 x1 x2 x3 x4 IN0. intros. destruct PR; [|right; apply H]. left. revert x0 x1 x2 x3 x4 H. pcofix CIH. intros. _punfold H0; [..|apply gpaco5_def_mon]. pstep. eapply gf_mon. apply H0. intros. apply rclo5_rclo. eapply rclo5_mon. apply PR. intros. destruct PR0. - apply rclo5_base. right. apply CIH. apply H. - destruct H; [destruct H|]. + apply rclo5_base. right. apply CIH0. left. apply H. + apply IN in H. destruct H. eapply rclo5_mon. apply IN0. intros. destruct PR0. * right. apply CIH. apply H. * right. apply CIH0. right. apply H. + apply rclo5_base. right. apply CIH0. right. apply H. Qed.
imports: Program.Basics Paco(paco5 pacotac)