Nuprl - Proof: intseg split 1

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

1. a :

2. b :

3. c : {a...b}

({a..c

}+{c..b

}) ~ {a..b

}

By:	Use:[{a..b} \| P(x):= x<c] Inst: Thm* (x:A. Dec(P(x))) (A ~ ({x:A\| P(x) }+{x:A\| P(x) }))

Generated subgoal:

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

About:

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