%%% Mapping evaluations to evaluations in environments.
%%% Version restricted to pure lambda-calculus
%%% Author: Frank Pfenning, based on [Hannan & Pfenning 92]

map_eval : eval E V -> trans K F E
	      -> feval K F W -> vtrans W V -> type.

mp_1 : map_eval (ev_lam) (tr_1 (vtr_lam (tr_lam C2)))
		(fev_1) (vtr_lam (tr_lam C2)).

mp_^ : map_eval D (tr_^ C1) (fev_^ D1') U1
	  <- map_eval D C1 D1' U1.

mp_lam : map_eval (ev_lam) (tr_lam C1)
		  (fev_lam) (vtr_lam (tr_lam C1)).

mp_app : map_eval (ev_app D3 D2 D1) (tr_app C2 C1)
	  (fev_app D3' D2' D1') U3
	  <- map_eval D1 C1 D1' (vtr_lam (tr_lam C3))
	  <- map_eval D2 C2 D2' U2
	  <- map_eval D3 (C3 W2 V2 U2) D3' U3.