IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iter via intseg null1 1. A : Type
2. f : AAA 3. u : A 4. a : 5. b : 6. e : {a..b}A 7. ba (Iter(f;u) i:{a..b}. e(i)) = u
By:
Compute Iter(f;u) i:{a..b}. e(i) = uA THEN SplitITE Concl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
}
a
(Iter(f;u) i:{a..b
Iter(f;u) i:{a..b
= u 
A THEN SplitITE Concl
