Ability to do sub-specified definitions.
If you want an object with propriety P(x), you can feed a proof of unique existence of Q(x) as long as Q is OL-smaller than P (so in particular it holds if Q=P/\S).
There is an example with a non-empty set in Exercise.scala.
Ability to do sub-specified definitions. If you want an object with propriety P(x), you can feed a proof of unique existence of Q(x) as long as Q is OL-smaller than P (so in particular it holds if Q=P/\S). There is an example with a non-empty set in Exercise.scala.