%
% is-value E  :  whether an exp E is a value
%

is-value : exp -> type.
%name is-value _IsVal.

is-value/unit  : is-value unit.

is-value/merge : is-value E1
              -> is-value E2
              -> is-value (merge E1 E2).

is-value/lam   : is-value (lam Ebody).

%freeze is-value.


%
% exp-not-app,   app-not-app
%

exp-not-app :       {E : exp} type.

exp-not-app/val :   is-value V -> exp-not-app V.
exp-not-app/merge : exp-not-app (merge E1 E2).


app-not-app :
   % If
        exp-not-app (app E1 E2)
   % then
     -> absurd
  -> type.
%mode app-not-app +NotApp -Absurd.

% All cases impossible

%worlds ()     (app-not-app _ _).
%total  NotApp (app-not-app NotApp _).