WhoCites
Definitions
mb
automata
2
Sections
GenAutomata
Doc
Who Cites pre
kind?
pre_kind
Def t.kind == 1of(t)
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
Syntax:
t.kind
has structure:
pre_kind(t)
About:
WhoCites
Definitions
mb
automata
2
Sections
GenAutomata
Doc
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p) 
AA:Type, B:(AType), p:(a:AB(a)). 1of(p) A
