IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ncompose zero1 1. 'a : Type
2. f : 'a'a 3. x : 'a 4. (0=0) = false f(ncompose(f;0-1;x)) = x
By:
Id THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'a
0) = false
f(ncompose(f;0-1;x)) = x
