proposition: Lemma monotone1_map (gf: rel1 T0 -> rel1 T0) (MON: _monotone1 gf) : _monotone (fun R0 => @uncurry1 T0 (gf (@curry1 T0 R0))).
proof: Proof. red; intros. apply uncurry_map1. apply MON; apply curry_map1; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)