Nuprl - Proof: card split prod intseg family 1 1

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

1. a :

2. b :

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

}

Type

((i:{a..b

} st i<c

B(i))

(i:{a..b

} st

i<c

B(i)))

((i:{a..c

}

B(i))

(i:{c..b

}

B(i)))

By:	BackThru: Thm* (A ~ A') (B ~ B') ((AB) ~ (A'B')) THEN OOCifExteq

Generated subgoals:

1 (i:{a..b} st i<cB(i)) =ext (i:{a..c}B(i))
1 step

2 (i:{a..b} st i<cB(i)) =ext (i:{c..b}B(i))
1 step

About:

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

1	(i:{a..b} st i<cB(i)) =ext (i:{a..c}B(i))	1 step
2	(i:{a..b} st i<cB(i)) =ext (i:{c..b}B(i))	1 step