PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map
is
nil
A
,
B
:Type,
f
:(
A
B
),
l
:
A
List. map(
f
;
l
) = nil
l
= nil
By:
InductionOnList THEN Reduce 0 THEN ObviousFrom [-1]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
A,B:Type, f:(A
B), l:A List. map(f;l) = nil 
l = nil A,B:Type, f:(AB), l:A List. map(f;l) = nil l = nil
