Nuprl - Proof: card split prod intseg family 1 1 2

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

1. a :

2. b :

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

}

Type

(i:{a..b

} st

i<c

B(i)) =ext (i:{c..b

}

B(i))

By:

Analyze

Generated subgoals:

None

About:

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