<p><span class="h-card" translate="no"><a href="https://mastodon.social/@whitequark" class="u-url mention">@<span>whitequark</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@lenary" class="u-url mention">@<span>lenary</span></a></span> <span class="h-card" translate="no"><a href="https://hachyderm.io/@unlambda" class="u-url mention">@<span>unlambda</span></a></span> ok now let me try to do undef.</p><p>on the source side, undef can yield any legal value and you need a \forall to model that. </p><p>on the target side, the rewrite is valid if any legal value makes it work, so there you need an \exists. </p><p>then there's one more wrinkle....</p>
