In Section  we gave an overview of existential relaxed noninterference (ERNI), explaining how it depends on type-based equivalences. To formally capture these type-based equivalences, we define a logical relation, defined by induction on the structure of types. To account for type variables, we build upon prior work on logical relations for parametricity [1]}, [2]}, [3]}. Then, we formally define ERNI on top of this logical relation. Finally, we prove that the type system of \(\mathsf {\lambda }^{\exists }_{\mathsf {SEC}}\)  enforces existential relaxed noninterference.
