[Security type soundness]theoremsecTypeSoundness

\(\Delta ;\Gamma \vdash e : S \Rightarrow \mathsf {ERNI}(\Delta ,\Gamma ,e,S)\) 


By induction on the typing derivation of \(e\) .
Following [1]}, we define a compatibility lemma for each typing rule; then, each case of the induction directly follows from the corresponding compatibility lemma.
