Module Qcert.Translation.Lang.NNRCtocNNRC

Require Import String.
Require Import List.
Require Import DataRuntime.
Require Import NNRC.
Require Import cNNRC.

Section NNRCtocNNRC.
  Context {fr:foreign_runtime}.

  Section Top.
    Context (h:brand_relation_t).

    Definition nnrc_to_nnrc_core_top (q:nnrc) : nnrc_core :=
      nnrc_to_nnrc_core q.

    Theorem nnrc_to_nnrc_core_top_correct :
      forall q:nnrc, forall global_env:bindings,
          nnrc_eval_top h q global_env =
          nnrc_core_eval_top h (nnrc_to_nnrc_core_top q) global_env.
  End Top.
    
End NNRCtocNNRC.