exp : env P -> term P -> type.

exp_empty   : exp empty lunit.
exp_addv    : exp (addv G X) (lpair N X)
	    <- exp G N.

invcav : absv G X F -> conc F M -> exp G N -> conv (M N) X -> type.

invcav_x    : invcav av_x csnd (exp_addv EP) c_prr.

invcav_y    : invcav (av_y AV) (ccomp (CP:conc _ M) cfst) 
	             (exp_addv EP:exp _ (lpair MG Y))
                     (c_trans (CC (c_prl:conv (lfst (lpair MG Y)) _)) CVP)
	    <- cong M CC 
	    <- invcav AV CP EP CVP.

invca : abse G E F -> conc F M -> exp G N -> conv (M N) E -> type.

invca_var   : invca (avar AV) CP EP CVP 
	    <- invcav AV CP EP CVP.

invca_fst   : invca (afst AP) (ccomp cfst CP) EP (c_fst CVP)
	    <- invca AP CP EP CVP.

invca_snd   : invca (asnd AP) (ccomp csnd CP) EP (c_snd CVP)
	    <- invca AP CP EP CVP.

invca_pair  : invca (apair AP1 AP2) (cpair CP1 CP2) EP (c_pair CVP1 CVP2)
	    <- invca AP1 CP1 EP CVP1
	    <- invca AP2 CP2 EP CVP2.

invca_lam   : invca (alam ([x] AP x)) (ccur CP) EP (c_lam ([x] CVP x))
	    <- {x}invca (AP x) CP (exp_addv EP) (CVP x).

invca_app   : invca (aapp AP1 AP2) (ccomp capp (cpair CP1 CP2)) EP 
	            (c_app (c_trans c_prl CVP1) (c_trans c_prr CVP2))
	    <- invca AP1 CP1 EP CVP1
	    <- invca AP2 CP2 EP CVP2.

% sigma[p1:{x}{y}abse (addv (addv empty x) y) x F] sigma [p2:conc F M] sigma [p3:{x}{y}exp (addv (addv empty x) y) (N x y)] {x}{y}invca (p1 x y) p2 (p3 x y) (R x y).

% sigma[p1:{x}abse (addv empty x) (llam [y] lpair y x) F] sigma [p2:conc F M] sigma [p3:{x}exp (addv empty x) (N x)] {x}invca (p1 x) p2 (p3 x) (R x).

zconc : mor A B -> env A -> term B -> type.

zconc1 : zconc F G (M MG)
	<- conc F M
	<- exp G MG.

inv : abse G E F -> zconc F G E' -> conv E' E -> type.
	
inv1 : inv AP (zconc1 EXP CP) EE
	<- invca AP CP EXP EE.

% sigma[p1:{x}abse (addv empty x) (llam [y] lpair y x) F] sigma [p2:{x}zconc F (addv empty x) (M x)] {x} inv (p1 x) (p2 x) (R x).