Nuprl - Proof: intseg split 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: intseg split 1 1 1 1

1. a :

2. b :

3. c : {a...b}
4. {a..b

} ~ ({x:{a..b

}| x<c }+{x:{a..b

x<c })

{a..c

} =ext {x:{a..b

}| x<c }

By:

Analyze

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html