fact: Definition paco2(gf : rel2 T0 T1 -> rel2 T0 T1)(r: rel2 T0 T1) : rel2 T0 T1 := @curry2 T0 T1 (paco (fun R0 => @uncurry2 T0 T1 (gf (@curry2 T0 T1 R0))) (@uncurry2 T0 T1 r)).
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)