% Testing uniqueness declarations

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z Y Y.
ps : plus (s X) Y (s Z)
      <- plus X Y Z.
% p_z : plus X z X.

%mode plus +X +Y -Z.
%worlds () (plus X Y Z).
%unique plus +X +Y -1Z.

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

eq : exp -> exp -> type.

refl : eq E E.

copy : exp -> exp -> type.
clam : copy (lam [x] E x) (lam [x] F x)
	<- ({x:exp} copy x x -> copy (E x) (F x)).
capp : copy (app E1 E2) (app F1 F2)
	<- eq E1 E1'
	<- copy E1' F1
	<- copy E2 F2.

% %mode copy +E -1F.
%block cb : block {x:exp} {u:copy x x}.

%worlds (cb) (eq E F).
%worlds (cb) (copy E F).

% %block cb1 : block {x:exp} {u:copy x x} {u1:copy x x}.
% %worlds (cb | cb1) (copy E F).

% %block cb2 : block {x:exp} {u:copy x x} {u2:{E:exp} copy E x}.
% %worlds (cb | cb2) (copy E F).

% %block cb3 : block {x:exp} {u:{E:exp} copy (app x E) (app E E)}.
% %worlds (cb | cb3) (copy E F).

% %unique eq +E -F.
%unique eq +E -1F.
%unique copy +E -1F.