proposition: Lemma gpaco3_cofix clo r rg l (OBG: forall rr (INC: rg <3= rr) (CIH: l <3= rr), l <3= gpaco3 clo r rr): l <3= gpaco3 clo r rg.
proof: Proof. assert (IN: l <3= gpaco3 clo r (rg \3/ l)). { intros. apply OBG; [left; apply PR0 | right; apply PR0 | apply PR]. } clear OBG. intros. apply IN in PR. destruct PR. econstructor. eapply rclo3_mon. apply IN0. clear x0 x1 x2 IN0. intros. destruct PR; [|right; apply H]. left. revert x0 x1 x2 H. pcofix CIH. intros. _punfold H0; [..|apply gpaco3_def_mon]. pstep. eapply gf_mon. apply H0. intros. apply rclo3_rclo. eapply rclo3_mon. apply PR. intros. destruct PR0. - apply rclo3_base. right. apply CIH. apply H. - destruct H; [destruct H|]. + apply rclo3_base. right. apply CIH0. left. apply H. + apply IN in H. destruct H. eapply rclo3_mon. apply IN0. intros. destruct PR0. * right. apply CIH. apply H. * right. apply CIH0. right. apply H. + apply rclo3_base. right. apply CIH0. right. apply H. Qed.
imports: Program.Basics Paco(paco3 pacotac)