Benedikt Ahrens

I had produced these constructions for a talk on UF. (In the end, I did not even get to that part in my talk...) I don't have a strong opinion...

@peterlefanulumsdaine : as you anticipated, a merge conflict after merging #536 ...

What is the status of this issue, @mortberg @DanGrayson ? Can we close it?

@mortberg : solution to what? It is hence not just a matter of removing two lines? Then the title of the issue should be changed.

@mortberg : would you still like to have those two lines removed from `.dir_locals.el`? @DanGrayson : any comments?

lgtm - thanks, @peterlefanulumsdaine !

@DanGrayson @nmvdw @peterlefanulumsdaine : Is this issue done with @nmvdw ' s recent reorganization of OrderTheory?

This issue is solved, closing.

Thanks a lot for filing this PR. I have made a few small comments. Can you describe what the issue is with the admitted proof? You could add the axiom...

@DenSinH : do you have any questions about the suggestions made to this PR? Is anything unclear?