[Agda] PreorderReasoning not Polymorphic Enough?

[Nils Anders Danielsson]

On 1/7/08, Nils Anders Danielsson <nad at cs.chalmers.se> wrote:
>
> If you want this then I suggest that you add a preorder as an argument
> to the begin_ function, with suitable changes to the other functions.

I have now added a module Relation.Binary.PreorderReasoning.Flexible
which does what you want. Unfortunately this means that we have two
almost identical modules in the library. I do not want to remove the
previous interface, since it is quite common to use the same preorder
for a number of proofs in the same module. Any suggestions on how to
resolve this?

-- 
/NAD