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

About:
listlist_ind
universememberpropfalsetrueall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions hol list 1 Sections HOLlib Doc