Prove that uPred is complete even if we remove the validity restriction in uPred_closed.
I already tried to prove that earlier and failed. But it turns out this is actually possible, and makes the definition of the uPred OFE much clearer.
I also added a comment explaining that.
Left to do: explain that in the doc. What is currently there is wrong for two reasons:
1- It does contain validity in uPred_closed (i.e., it needs to be updated with respect to this MR)
2- The stuff explained in the doc about the alternate definition based on SProp is completely wrong (it is just not isomorphic to uPred).
Edited by Jacques-Henri Jourdan