[…]
But the proof function was saying the other way: given all values in a
character range, they can always be represented with this form of UTF-8
string. And for this, a relation between b1 and b2 was required, as c
imposes this relation. So your way was the only one possible for this proof
functions:
[…]
I tried to continue to investigate on my initial idea, and there is more. I
won’t tell all of of what get trough my mind, but it can be summarized.
Given this:
dataprop P =
| P1
dataprop Q =
| Q1 of P
One can say “if you have a P, you can get a Q”:
prfn pf (p:P): Q = Q1(p)
But although it could intuitively make sense, there is no way to say
something like “if you have a Q, you could got a P”:
// For the picture, not possible!
prfn pf (q:Q): [p:P; q == Q1(p)] void
Investigating more, I believe that’s also this kind of impasse, I was in.