ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label
, t:SimpleType. t 
dec_lookup(ds;x) 
s.x [[t]] rhods:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds y [[a]] rho| Theorem | Name |
|
Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label
, t:SimpleType. t dec_lookup(ds;x) s.x [[t]] rho | [record_select_wf_decls_mng2] |
| cites | |
|
Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x)
, a:SimpleType. mk_dec(x, a) ds y [[a]] rho | [decls_mng_subtype] |