% Value soundness

% Partial check of hand-coded proof
%terminates D (vs D _).

% Automatic proof generation
%theorem vls : forall* {E : exp} {V : exp} 
               forall {D : eval E V} 
               exists {P : value V} true.
%prove 3 D (vls D _).

% Partial verification of generated proof
%terminates D (vls D _).