Remark Definitions GenAutomata Sections NuprlLIB Doc

No mentions to report in GenAutomata
type_injDef [x]{T} == x
Thm* T:Type, E:(TTProp). (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:
quotientfunctionuniversememberpropimpliesall!abstraction

Remark Definitions GenAutomata Sections NuprlLIB Doc