Intrinsically typed syntax is an important and popular method for mechanized reasoning about programming languages. We explore the limits of this method in the setting of finitely-stratified System F using the Agda proof assistant. This system supports elegant definitions of denotational semantics as well as big-step operational semantics based on intrinsically typed syntax. While its syntactic metatheory (i.e., type soundness) works well, we demonstrate that its semantic metatheory poses technical challenges, by defining a logical relation and proving its fundamental lemma. Our logical relation connects a denotational semantics with an operational one, which exposes issues with transfer lemmas as well as minor issues with universe polymorphism.