proposition: Lemma gupaco0_mon_gen (gf' clo clo': rel -> rel) r r' (IN: @gupaco0 gf clo r) (gf_mon: monotone0 gf) (LEgf: gf <1= gf') (LEclo: clo <1= clo') (LEr: r <0= r'): @gupaco0 gf' clo' r'.
proof: Proof. eapply gpaco0_mon_gen. apply IN. apply gf_mon. apply LEgf. apply LEclo. apply LEr. apply LEr. Qed.
imports: Program.Basics Paco(paco0 pacotac)