grammar
1
Sections
AutomataTheory
Doc
g_init
Def
g.init == 2of(g)
Thm*
V,T:Type, g:Grammar(V;T). g.init
V
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:a:A
B(a). 2of(p)
B(1of(p))
About:
V,T:Type, g:Grammar(V;T). g.init 
VA:Type, B:(A
Type), p:a:A
B(a). 2of(p) B(1of(p))
