Nuprl - Proof: card split prod intseg family

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

a,b:

, c:{a...b}, B:({a..b

}

Type).

(i:{a..b

}

B(i)) ~ ((i:{a..c

}

B(i))

(i:{c..b

}

B(i)))

By:

Auto

Generated subgoal:

1 1. a :
2. b :
3. c : {a...b}
4. B : {a..b}Type
(i:{a..b}B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i)))
4 steps

About:

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