IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mt def mt(nil) = True & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False)
By:
Unab [`mt`] THEN Reduce 0 THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mt(nil) = True & (
'a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False)
