% Type preservation

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

%theorem
tpp : forall* {E: exp} {V: exp} {T: tp}
       forall {D: eval E V} {P: of E T} 
       exists {Q: of V T} true.

% prove 1 D (tpp D _ _).

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