WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites mt?
mt
Def mt(
l
) == Case of
l
; nil
True ;
a
.
as'
False
Thm*
'a
:Type{i},
l
:
'a
List. mt(
l
)
Prop{1}
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
True ; a.as' False
'a:Type{i}, l:'a List. mt(l) 
Prop{1} True ; a.as' False'a:Type{i}, l:'a List. mt(l) Prop{1}
