We show how to reason about "step-indexed" logical relations in an
abstract way, avoiding the tedious, error-prone, and proof-obscuring
step-index arithmetic that seems superficially to be an essential
element of the method. Specifically, we define a logic LSLR,
which is inspired by Plotkin and Abadi's logic for parametricity, but
also supports recursively defined relations by means of the modal
"later" operator from Appel et al.'s "very modal model" paper. We
encode in LSLR a logical relation for reasoning
(in-)equationally about programs in call-by-value System F extended
with recursive types. Using this logical relation, we derive a useful
set of rules with which we can prove contextual (in-)equivalences
without mentioning step indices.