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

lt : nat -> nat -> type.
lt/z : lt z (s N).
lt/s : lt (s N) (s M)
        <- lt N M.

loc : type.
left : loc.
right : loc.
adj : loc -> loc -> type.
at : loc -> nat -> type.

% sort : at L E * adj L L' * at L' E' * lt E' E
%          -o {at L E' * at L' E}.

l1 : loc.
l2 : loc.
l3 : loc.
- : adj left l1.
- : adj l1 l2.
- : adj l2 l3.
- : adj l3 right.

n0 : nat = z.
n1 : nat = s z.
n2 : nat = (s (s z)).
n3 : nat = (s (s (s z))).

init : type = 
    {at left n2 * at l1 n3 * at l2 n2 * at l3 n0 * at right n1}.

#trace * init.

%% shuffler

member : nat -> type.
unused : loc -> type.

shuff : member X * unused L -o {at L X}.

init_shuff : type = 
    {member n0 * member n1 * member n3 * member n3 * member n2 * 
    unused left * unused l1 * unused l2 * unused l3 * unused right}.

#trace * init_shuff.

#query * * * 3 init_shuff -o {at left X0 * at l1 X1 * at l2 X2 * at l3 X3 *
at right Xright}.