Nuprl - Proof: card split end sum intseg family 1

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

1. a :

2. b :

3. B : {a..b

}

Type
4. a<b

(i:{a..b

}

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

}

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

By:	Use:[c:= b-1] Rewrite by Thm* a,b:, c:{a...b}, B:({a..b}Type). Thm* (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))

Generated subgoal:

1 ((i:{a..(b-1)}B(i))+(i:{(b-1)..b}B(i))) ~ ((i:{a..(b-1)}B(i))+B(b-1))
2 steps

About:

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