{-# OPTIONS --rewriting #-}
module Reflect4 where

import DS
import DSK
import CPS
import Reflect4a
import Reflect4b
open import DS-DSK
open import DSK-DS
open import DSK-CPS
open import CPS-DSK
open import TypeIsos

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality


-- main theorem
correctE : {var : Set} {Δ : CPS.Delta} →
           {e e' : CPS.term[ var , Δ ]} →
           CPS.Reduce e e' →
           DS.Reduce {var} (embE (dskE e)) (embE (dskE e'))
correctE red = Reflect4b.correctE (Reflect4a.correctE red)