Logical relation with fundamental theorem and logical compatibility lemmas
For example, the lemmas in https://gitlab.mpi-sws.org/iris/examples/blob/master/theories/logrel/F_mu_ref/fundamental_binary.v use meta-level implication. These should all be strengthened magic wands.
On the other hand, the logical relation on logrel_heaplang does not have a syntactic type system, and hence no fundamental lemma proven in Coq.
Edited by Ralf Jung