IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split int domain by norm lower12 1. P : Prop
2. a : 3. b:{...a}. P(a,a) P(a,b)
4. b:{a...}. P(a,b)
5. b : 6. ba P(a,b)
By:
BackThru: Hyp:4
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
b:{...a}. P(a,a) 
P(a,b)
b
a
P(a,b)
