1 | 1. ds: Collection(dec()) 2. da: Collection(dec()) 3. de: sig() 4. rho: Decl 5. st1: Collection(SimpleType) 6. e1: {1of([[de]] rho)} 7. s: {[[ds]] rho} 8. a: [[st1]] rho 9. tr: trace_env([[da]] rho) l:Term List.
( i: ||l||. trace_consistent(rho;da;tr.proj;l[i])) 
( ls:SimpleType List, f:reduce( s,m. [[s]] rho m;Prop;ls).
||ls|| = ||l|| & ( i: . i < ||l||  ls[i] term_types(ds;st1;de;l[i])) 
list_accum(x,t.x([[t]] e1 s a tr);f;l) Prop) |