I:Type, A:(Iioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:{[[ioa_all(I; i.A(i)).ds]] rho}, i:I. s [[A(i)]] rho de e.state

1	1. I: Type 2. A: Iioa{i:l}() 3. rho: Decl 4. de: sig() 5. e: {[[de]] rho} 6. s: {[[ioa_all(I; i.A(i)).ds]] rho} 7. i: I s [[A(i)]] rho de e.state
2	1. I: Type{i} 2. A: Iioa{i:l}() 3. rho: Decl{i} 4. de: sig() 5. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho) 6. zzz: Decl{i}Decl{i'} Decl{i} Decl{i'}

About: