IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fun thru ite S,T:Type, f:(ST), b:, p,q:S.
f(if bp else q fi) = if bf(p) else f(q) fi
By:
RepD THEN (OnVar `b' BoolCases) THEN (AbReduce 0)
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
S,T:Type, f:(S
T), b:
, p,q:S.
f(if b
p else q fi) = if b
