% Completeness proof.
% If nd A then check M A.
ndToAnn: nd A -> check M A -> type.
%mode ndToAnn +D -E.

n_true: ndToAnn (nd_truei) (a_trueI).

n_andI: ndToAnn D1 E1 -> ndToAnn D2 E2
       -> ndToAnn (nd_andi D1 D2) (a_andI E1 E2).
     
n_andE1: ndToAnn D1 E1
       -> ndToAnn (nd_andel D1) (a_andE1 E1).

n_andE2: ndToAnn D1 E1
       -> ndToAnn (nd_ander D1) (a_andE2 E1).

n_impI: ({u:nd A}{x:term}{v:check x A}
         ndToAnn u v -> ndToAnn (D u) (E x v))
        -> ndToAnn (nd_impi [u:nd A] D u) (a_impI [x:term][u:check x A] E x u).

n_impE: 
        ndToAnn D1 E1 -> ndToAnn D2 E2 
        -> ndToAnn (nd_impe D1 D2) (a_impE E1 E2).

%terminates D (ndToAnn D E).
%block l : some {A:prop} block {u:nd A}{x:term}{v:check x A}{p: ndToAnn u v}.
%worlds (l) (ndToAnn D E).
%covers ndToAnn +D -E.
%total D (ndToAnn D E).