decl_type(d;l)
D:(IDecl), j:I, z:{D(i) for i 
I}. z {D(j)}
d) == l:Label
decl_type(d;l)D:(IDecl), j:I, z:(D(i) for i I). z (D(j)){2of(p)}| def | record | {d} == l:Labeldecl_type(d;l) |
| THM | rall_subtype | D:(IDecl), j:I, z:{D(i) for i I}. z {D(j)} |
| def | r_select | r.l == r(l) |
| def | sigma | (d) == l:Labeldecl_type(d;l) |
| THM | sall_subtype | D:(IDecl), j:I, z:(D(i) for i I). z (D(j)) |
| def | kind | kind(a) == 1of(a) |
| def | value | value(a) == 2of(a) |
| def | record_pair | {p} == {1of(p)}{2of(p)} |