proposition: Lemma gpaco4_weaken clo r rg: gpaco4 (gupaco4 clo) r rg <4= gpaco4 clo r rg.
proof: Proof. intros. apply gpaco4_unfold in PR. induction PR. - destruct IN; cycle 1. apply gpaco4_base, H. apply gpaco4_step_gen. eapply gf_mon. apply H. clear x0 x1 x2 x3 H. eapply gpaco4_cofix. intros. apply gpaco4_unfold in PR. induction PR. + destruct IN; cycle 1. apply gpaco4_base, H. apply gpaco4_step. eapply gf_mon. apply H. intros. apply gpaco4_base. apply CIH. eapply gupaco4_mon. apply PR. intros. destruct PR0; apply H0. + apply gpaco4_gupaco. eapply gupaco4_mon. apply IN. apply H. - apply gpaco4_gupaco. eapply gupaco4_mon. apply IN. apply H. Qed.
imports: Program.Basics Paco(paco4 pacotac)