(3steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
mt
1
1.
'a
: Type
2.
l
:
'a
List
Dec(mt(
l
))
By:
Unab [`decidable`;`mt`]
Generated subgoal:
1
(Case of
l
; nil
True ;
a
.
as'
False)
(Case of
l
; nil
True ;
a
.
as'
False)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
Dec(mt(l)) Dec(mt(l)) (Case of l; nil 
True ; a.as' False)
(Case of l; nil True ; a.as' False)
