WhoCites
Definitions
mb
automata
2
Sections
GenAutomata
Doc
Who Cites kind?
kind
Def kind(a) == 1of(a)
Thm*
d:Decl, a:(
d). kind(a)
Label
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
About:
WhoCites
Definitions
mb
automata
2
Sections
GenAutomata
Doc
d:Decl, a:(
d). kind(a) 
LabelA:Type, B:(A
Type), p:(a:A
B(a)). 1of(p) Ad:Decl, a:(d). kind(a) LabelA:Type, B:(AType), p:(a:AB(a)). 1of(p) A
