%Equality preservation for lambda-calc

ctoe : conv E E' -> abse G E F -> abse G E' F' -> F == F' -> type.

ctoe_refl   : ctoe c_refl AP AP refl.

ctoe_trans  : ctoe (c_trans CP1 CP2) AP1 AP2 (EP1 then EP2)
 	    <- ctoe CP1 AP1 AP3 EP1
	    <- ctoe CP2 AP3 AP2 EP2.

ctoe_sym    : ctoe (c_sym CP) AP1 AP2 (sym EP)
 	    <- ctoe CP AP2 AP1 EP.


ctoe_fst    : ctoe (c_fst CP) (afst AP) (afst AP') (=@= refl EP)
	    <- ctoe CP AP AP' EP.

ctoe_snd    : ctoe (c_snd CP) (asnd AP) (asnd AP') (=@= refl EP)
	    <- ctoe CP AP AP' EP.

ctoe_pair   : ctoe (c_pair CP1 CP2) (apair AP1 AP2) 
	    	   (apair AP1' AP2') (=pair= EP1 EP2)
	    <- ctoe CP1 AP1 AP1' EP1
	    <- ctoe CP2 AP2 AP2' EP2.

ctoe_lam    : ctoe (c_lam ([x] CP x)) (alam ([x] AP x))
	           (alam ([x] AP' x)) (=cur= EP)
	    <- {x}ctoe (CP x) (AP x) (AP' x) EP.

ctoe_app    : ctoe (c_app CP1 CP2) (aapp AP1 AP2) 
	           (aapp AP1' AP2') (=@= refl (=pair= EP1 EP2))
	    <- ctoe CP1 AP1 AP1' EP1
	    <- ctoe CP2 AP2 AP2' EP2.


ctoe_unit   : ctoe c_unit aunit AP (sym term_u).

ctoe_prl    : ctoe c_prl (afst (apair AP1 AP2)) AP1 prod_l.

ctoe_prr    : ctoe c_prr (asnd (apair AP1 AP2)) AP2 prod_r.

ctoe_surj   : ctoe c_surj (apair (afst AP) (asnd AP)) AP prod_u.

ctoe_beta   : ctoe c_beta (aapp (alam ([x] AP1 x)) AP2) AP
                   (=@= refl (=pair= (sym id_r) refl)
	            then EE
	            then EP)
	    <- subst AP2 AP1 AP EP
	    <- appl EE.

ctoe_eta    : ctoe c_eta (alam ([x] aapp (AP x) (avar av_x))) AP'
		   (=cur= (=@= refl (=pair= (sym EP) refl))
		    then exp_u)
	    <- {x}weak AP' (AP x) EP.

%sigma[p1:{f}abse (addv empty f) (llam [x] lapp f x) M1] sigma [p2:{f}abse (addv empty f) f M2] {f} ctoe c_eta (p1 f) (p2 f) E.

%sigma[p1:abse empty (llam [x] lapp (llam[y]y) x) M1] sigma [p2:abse empty (llam[y]y) M2]  ctoe c_eta p1 p2 E.

%sigma[p1:abse empty (llam [x] lapp (llam[f]llam[y]lapp f y) x) M1] sigma [p2:abse empty (llam[f]llam[y]lapp f y) M2]  ctoe c_eta p1 p2 E.

%sigma[p1:abse empty (llam[y]y) M1] sigma [p2:{x}abse (addv empty x) (llam[y]y) M2] {x}weak p1 (p2 x) E.

%sigma[p1:abse empty (llam [x] lapp (llam[f]llam[y]lapp f y) x) M1] sigma [p2:abse empty (llam[x]llam[y]lapp x y) M2]  ctoe (c_lam ([x]c_beta)) p1 p2 E.

%sigma[p1:abse empty (llam [x] lapp (llam[f]llam[y]lapp f y) x) M1] sigma [p2:abse empty (llam[x]x) M2]  ctoe (c_lam ([x]c_trans c_beta c_eta)) p1 p2 E.

%sigma[p1:abse empty (llam [x] lapp (llam[f]llam[y]lapp f y) (llam[z]lapp z x)) M1] sigma [p2:abse empty (llam[x]llam[y]lapp y x) M2]  ctoe (c_lam ([x]c_trans c_beta (c_lam [x] c_beta))) p1 p2 E. %(uses 28 meg, 60 sec)