% 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).