Nuprl - Proof: intseg split 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: intseg split 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

}+{c..b

}) ~ {a..b

}

By:	Rewrite by Hyp:-1

Generated subgoal:

1 ({a..c}+{c..b}) ~ ({x:{a..b}| x<c }+{x:{a..b}| x<c })
3 steps

About:

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