proposition: Lemma monotone2_map (gf: rel2 T0 T1 -> rel2 T0 T1) (MON: _monotone2 gf) : _monotone (fun R0 => @uncurry2 T0 T1 (gf (@curry2 T0 T1 R0))).
proof: Proof. red; intros. apply uncurry_map2. apply MON; apply curry_map2; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)