IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card boolset vs mset13211 1. a : 2. k : 3. (p,i. if p(i) 1 else 0 fi) (a {k})a {k}2
4. (f,i. f(i)=1) (a {k}2)a {k} 5. f : a2
6. Msize(f) = k 7. x : a if f(x)=1 1 else 0 fi = f(x) 2
By:
SplitITE Concl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html