<p><span class="h-card" translate="no"><a href="https://types.pl/@ionchy" class="u-url mention">@<span>ionchy</span></a></span> ok but here the \lam is at the term level, not the type level right?</p>