<p><span class="h-card" translate="no"><a href="https://types.pl/@ionchy" class="u-url mention">@<span>ionchy</span></a></span> mostly trying to get into the weeds of LF / CoC so kind of both ? but LF for now so predicative</p><p>what im getting is "you can't construct x : T if x : \forall T. T" but im trying to concretize it</p>
