Remark
Definitions
GenAutomata
Sections
NuprlLIB
Doc
No mentions to report in GenAutomata
type_inj
Def [x]{T} == x
Thm*
T:Type, E:(T
T
Prop). (EquivRel x,y:T. E(x,y))
(
a:T. [a]{x,y:T//E(x,y)}
x,y:T//E(x,y))
Syntax:
[x]{T}
has structure:
type_inj(x; T)
About:
Remark
Definitions
GenAutomata
Sections
NuprlLIB
Doc