proposition: Lemma gpaco0_mon_gen (gf' clo clo': rel -> rel) r r' rg rg' (IN: @gpaco0 gf clo r rg) (gf_mon: monotone0 gf) (LEgf: gf <1= gf') (LEclo: clo <1= clo') (LEr: r <0= r') (LErg: rg <0= rg') : @gpaco0 gf' clo' r' rg'.
proof: Proof. eapply gpaco0_mon; [|apply LEr|apply LErg]. destruct IN. econstructor. eapply rclo0_mon_gen. apply IN. apply LEclo. intros. destruct PR; [| right; apply H]. left. eapply paco0_mon_gen. apply H. - intros. eapply LEgf. eapply gf_mon. apply PR. intros. eapply rclo0_mon_gen. apply PR0. apply LEclo. intros; apply PR1. - intros. apply PR. Qed.
imports: Program.Basics Paco(paco0 pacotac)