Nuprl - Proof: card prod family intseg singleton elim 1

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

1. a :

2. a' :

3. a'-a = 1
4. B : {a..a'

}

Type

(i:{a..a'

}

B(i)) ~ B(a)

By:	a {a:} \| B {a:}Type Asserted

Generated subgoals:

1   a  {a:}
1 step

2 5. a  {a:}
  B  {a:}Type
2 steps

3 5. a  {a:}
6. B  {a:}Type
  (i:{a..a'}B(i)) ~ B(a)
4 steps

About:

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