Nuprl - Proof: card split sum intseg family 1 1

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

1. a :

2. b :

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

}

Type
5. (i:{a..b

}

B(i)) ~ ((i:{i:{a..b

}| i<c }

B(i))+(i:{i:{a..b

i<c }

B(i)))

((i:{i:{a..b

}| i<c }

B(i))+(i:{i:{a..b

i<c }

B(i)))

((i:{a..c

}

B(i))+(i:{c..b

}

B(i)))

By:	BackThru: Thm* (A ~ A') (B ~ B') ((A+B) ~ (A'+B'))

Generated subgoals:

1 (i:{i:{a..b}| i<c }B(i)) ~ (i:{a..c}B(i))
1 step

2 (i:{i:{a..b}| i<c }B(i)) ~ (i:{c..b}B(i))
1 step

About:

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

1	(i:{i:{a..b}\| i<c }B(i)) ~ (i:{a..c}B(i))	1 step
2	(i:{i:{a..b}\| i<c }B(i)) ~ (i:{c..b}B(i))	1 step