Nuprl - Proof: card split sum intseg family 1 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

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:{a..c

}

B(i))

By:	OOCifExteq THEN Analyze

Generated subgoals:

None

About:

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