Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma. - Hannes Saffrich; Peter Thiemann 001; Marius Weidner (TyDe@ICFP, 2024)