2. da: Collection(dec())
3. st: Collection(SimpleType)
4. de: sig()
5. rho: Decl
6. e1: {1of([[de]] rho)}
7. s1: {[[ds]] rho}
8. s2: {[[ds]] rho}
9. a: [[st]] rho
10. tr: trace_env([[da]] rho)
11. u: Term
t:SimpleType.
trace_consistent(rho;da;tr.proj;u) 
(x:Label. (x 
term_vars(u)) s1.x = s2.x)
t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho
