IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
mt(nil) = True & (
'a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False)
