mb
record
Sections
GenAutomata
Doc
Def
{d} == l:Label
decl_type(d;l)
is mentioned by
Thm*
D:(I
Decl), j:I, z:{D(i) for i
I}. z
{D(j)}
[rall_subtype]
Def
{p} == {1of(p)}
{2of(p)}
[record_pair]
Try larger context:
GenAutomata
mb
record
Sections
GenAutomata
Doc
D:(I
Decl), j:I, z:{D(i) for i 
I}. z {D(j)}
{2of(p)}decl_type(d;l)
D:(IDecl), j:I, z:{D(i) for i I}. z {D(j)}{2of(p)}