Module Qcert.Translation.NRAEnvtocNRAEnv


Section NRAEnvtocNRAEnv.
  Require Import String.
  Require Import List.
  Require Import CommonRuntime.
  Require Import NRAEnvRuntime.
  Require Import cNRAEnvRuntime.

  Context {fr:foreign_runtime}.

  Section Top.
    Context (h:brand_relation_t).

    Definition nraenv_to_nraenv_core_top (q:nraenv) : nraenv_core :=
      nraenv_to_nraenv_core q.

    Theorem nraenv_to_nraenv_core_top_correct :
      forall q:nraenv, forall global_env:bindings,
          nraenv_eval_top h q global_env =
          nraenv_core_eval_top h (nraenv_to_nraenv_core_top q) global_env.
Proof.
      intros.
      unfold nraenv_core_eval_top.
      unfold nraenv_eval_top.
      unfold nraenv_to_nraenv_core_top.
      unfold nraenv_eval.
      reflexivity.
    Qed.
  End Top.
    
End NRAEnvtocNRAEnv.