Nuprl - Proof: card split end sum intseg family 1 1 1

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

1. a :

2. b :

3. B : {a..b

}

Type
4. a<b

(i:{(b-1)..b

}

B(i)) ~ B(b-1)

By:	BackThru: Thm* a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))

Generated subgoals:

None

About:

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