%%% Equivalence between soundness and completeness proofs
%%% Author: Frank Pfenning

peq : csd C D C'
       -> ccp D C' C
       -> type.

% Natural Numbers
peq_z : peq (csd_z) (ccp_z).
peq_s : peq (csd_s SD1) (ccp_s CP1)
	 <- peq SD1 CP1.
peq_case_z : peq (csd_case_z SD2 SD1) (ccp_case_z CP1 CP2)
	      <- peq SD1 CP1
	      <- peq SD2 CP2.
peq_case_s : peq (csd_case_s SD3 SD1) (ccp_case_s CP1 CP3)
	      <- peq SD1 CP1
	      <- peq SD2 CP2.

% Pairs
peq_pair : peq (csd_pair SD2 SD1) (ccp_pair CP1 CP2)
	    <- peq SD1 CP1
	    <- peq SD2 CP2.
peq_fst  : peq (csd_fst SD1) (ccp_fst CP1)
	    <- peq SD1 CP1.
peq_snd  : peq (csd_snd SD1) (ccp_snd CP1)
	    <- peq SD1 CP1.

% Functions
peq_lam : peq (csd_lam) (ccp_lam).
peq_app : peq (csd_app SD3 SD2 SD1) (ccp_app CP1 CP2 CP3)
	   <- peq SD1 CP1
	   <- peq SD2 CP2
	   <- peq SD3 CP3.

% Definitions
peq_letv : peq (csd_letv SD2 SD1) (ccp_letv CP1 CP2)
	    <- peq SD1 CP1
	    <- peq SD2 CP2.

peq_letn : peq (csd_letn SD1) (ccp_letn CP1)
	    <- peq SD1 CP1.

% Recursion
peq_fix : peq (csd_fix SD1) (ccp_fix CP1)
	   <- peq SD1 CP1.

% Values
peq_vl : peq (csd_vl) (ccp_vl).


%%% For complete evaluations

proof_equiv : ceval_sound CE D -> ceval_complete D CE -> type.

pequiv : proof_equiv (cevsd SD) (cevcp CP)
	  <- peq SD CP.