r:rel(), rho:Decl, ds,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, a1,a2:Top, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r) 
tc(r;ds;da1;de) closed_rel(r) ([[r]] rho ds da1 de e s a1 tr 
[[r]] rho ds da2 de e s a2 tr)r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de)v:Top, rho:Decl. v 
[[ < > ]] rhol1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil