WhoCites
Definitions
mb
automata
1
Sections
GenAutomata
Doc
Who Cites rel
args?
rel_args
Def t.args == 2of(t)
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
Syntax:
t.args
has structure:
rel_args(t)
About:
WhoCites
Definitions
mb
automata
1
Sections
GenAutomata
Doc