Thms
relation
autom
Sections
AutomataTheory
Doc
compose
Def
(f o g)(x) == f(g(x))
Thm*
A,B,C:Type, f:(B
C), g:(A
B). f o g
A
C
tidentity
Def
Id == Id
Thm*
A:Type. Id
A
A
identity
Def
Id(x) == x
Thm*
A:Type. Id
A
A
About:
A,B,C:Type, f:(B
C), g:(AB). f o g 
ACA:Type. Id AAA:Type. Id AA
