2 | 14. i: (||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i]) 15. ls: SimpleType List 16. f: reduce( s,m. [[s]] rho m;Prop;ls) 17. ||ls|| = ||v||+1  18. i: . i < ||v||+1  ls[i] term_types(ds;st1;de;[u / v][i]) 19. ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||v|| & ( i: . i < ||v||  ls[i] term_types(ds;st1;de;v[i])) 
list_accum(x,t.x([[t]] e1 s s' a tr);f;v) Prop list_accum(x,t.x([[t]] e1 s s' a tr);f([[u]] e1 s s' a tr);v) Prop |