rho:Decl, ds,daa:Collection(dec()), da1:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, tr:trace_env([[daa]] rho), r:rel(). closed_rel(r) 
tc(r;ds;da1;de) 2. ds: Collection(dec())
3. daa: Collection(dec())
4. da1: Collection(SimpleType)
5. de: sig()
6. s: {[[ds]] rho}
7. e: {[[de]] rho}
8. tr: trace_env([[daa]] rho)
9. r: rel()
10. closed_rel(r)
11. tc(r;ds;da1;de)
12. trace_consistent_rel(rho;daa;tr.proj;r)
[[r]] rho ds da1 de e s 
tr 
Prop
