WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites tidentity?
tidentity
Def Id == Id
Thm*
A:Type. Id
A
A
identity
Def
Id(x) == x
Thm*
A:Type. Id
A
A
Syntax:
Id
has structure:
tidentity(T)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
A:Type. Id 
A
AA:Type. Id AAA:Type. Id AAA:Type. Id AA
