proposition: Theorem _paco11_mult_strong: forall r, paco11 gf (upaco11 gf r) <11== paco11 gf r.
proof: Proof. intros. apply curry_map11. eapply le1_trans; [| eapply _paco_mult_strong]. apply _paco_mon; intros [] H; apply H. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)