proposition: Lemma monotone0_map (gf: rel0 -> rel0) (MON: _monotone0 gf) : _monotone (fun R0 => @uncurry0 (gf (@curry0 R0))).
proof: Proof. red; intros. apply uncurry_map0. apply MON; apply curry_map0; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)