proposition: Lemma upaco0_mon_bot (gf gf': rel0 -> rel0) r' (REL: upaco0 gf bot0) (LEgf: gf <1= gf'): upaco0 gf' r'.
proof: Proof. eapply upaco0_mon_gen; [apply REL | apply LEgf | intros; contradiction PR]. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)