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

2. b :

3. B : {a..b

}

Type
4. a<b

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

}

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

}

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

}

B(i))+B(b-1))

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

Generated subgoal:

1 (i:{(b-1)..b}B(i)) ~ B(b-1)
1 step

About:

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