proposition: Theorem _paco11_fold: forall r, gf (upaco11 gf r) <11== paco11 gf r.
proof: Proof. intros. apply uncurry_adjoint1_11. eapply le1_trans; [| apply _paco_fold]. apply le1_refl. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)