proposition: Lemma gpaco9_unfold clo r rg: gpaco9 clo r rg <9= rclo9 clo (gf (gupaco9 clo (rg \9/ r)) \9/ r).
proof: Proof. intros. destruct PR. eapply rclo9_mon. apply IN. intros. destruct PR; cycle 1. right; apply H. left. _punfold H; [|apply gpaco9_def_mon]. eapply gf_mon. apply H. intros. econstructor. eapply rclo9_mon. apply PR. intros. destruct PR0; cycle 1. right. apply H0. left. eapply paco9_mon. apply H0. intros. left. apply PR0. Qed.
imports: Program.Basics Paco(paco9 pacotac)