Qcert.NRAEnv.Typing.TcNRAEnvIgnore

Section TcNRAEnvIgnore.







  Lemma tcnraenv_ignores_env_swap {m:basic_model} (e:cnraenv) :
    cnraenv_ignores_env e →
    ∀ τc (τin τout τenv₁ τenv₂:rtype),
    e ▷ τin >=> τout ⊣ τc;τenv₁ → e ▷ τin >=> τout ⊣ τc;τenv₂.

  Lemma tcnraenv_ignores_id_swap {m:basic_model} (e:cnraenv) :
    cnraenv_ignores_id e →
    ∀ τc (τin₁ τin₂ τout τenv:rtype),
    e ▷ τin₁ >=> τout ⊣ τc;τenv → e ▷ τin₂ >=> τout ⊣ τc;τenv.

End TcNRAEnvIgnore.