<p><span class="h-card" translate="no"><a href="https://mathstodon.xyz/@rg9119" class="u-url mention">@<span>rg9119</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@andrejbauer" class="u-url mention">@<span>andrejbauer</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention">@<span>MartinEscardo</span></a></span> is this what&#39;s colloquially meant by &quot;proof relevance&quot;, or is that something else?</p>