proposition: Lemma gpaco0_mon_bot (gf' clo clo': rel -> rel) r' rg' (IN: @gpaco0 gf clo bot0 bot0) (gf_mon: monotone0 gf) (LEgf: gf <1= gf') (LEclo: clo <1= clo'): @gpaco0 gf' clo' r' rg'.
proof: Proof. eapply gpaco0_mon_gen. apply IN. apply gf_mon. apply LEgf. apply LEclo. contradiction. contradiction. Qed.
imports: Program.Basics Paco(paco0 pacotac)