% Testing subordination and worlds

%{
a : type.
b : a -> type.

c : a -> type.

d : {x:a} b x -> c x -> type.

% Next line leads to subordination error since  b not <| c

%worlds (pi {x:a} {y:b x -> c x} {z:c x -> b x}) (d _ _ _).
}%

nat : type.				%name nat N.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.	%name plus P.
pz : plus z N N.
ps : plus (s M) N (s P)
      <- plus M N P.
%worlds () (plus N M P).

exp : type.				%name exp E x.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

copy : exp -> exp -> type.		%name copy C u.
clam : copy (lam E) (lam F)
	<- ({x:exp} copy x x -> copy (E x) (F x))
        <- plus z z P.
% next line make subordination fail because
% it implies exp <| plus
%        <- ({x:exp} plus z z P)

capp : copy (app E1 E2) (app F1 F2)
	<- copy E1 F1
	<- copy E2 F2.

%worlds (pi {x:exp} {u:copy x x}) (copy E F).