%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This elf file implements an list data type.
% proj_exp (cons_exp (psd (s (s z))) nil_exp) z E.
% append_exp (psd (s (s z))) nil_exp L N.
% count_exp (cons_exp (psd (s (s z))) nil_exp) N.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

exp : type.
exps : type.

nil_exp : exps.
cons_exp : exp -> exps -> exps.

%abbrev $exp = cons_exp. %infix right 10 $exp.

proj_exp : exps -> nat -> exp -> type.
%mode proj_exp +EL +N -E.
proj_exp_z : proj_exp (cons_exp E EL) z E.
proj_exp_s : proj_exp (cons_exp E EL) (s N) E'
	      <- proj_exp EL N E'.

update_exp : exps -> exp -> nat -> exps -> exp -> type.
%mode update_exp +EL +E +N -EL' -E.
update_exp_z : update_exp (cons_exp E' EL) E z (cons_exp E EL) E'.
update_exp_s : update_exp (cons_exp E' EL) E (s N) (cons_exp E' EL') E''
		<- update_exp EL E N EL' E''.