Nuprl - Pf discrete product 1 1 1 4 1 1

1. T1: Type{i}
2. T2: Type{j}
3. x1: T1
4. x2: T2
5. y1: T1
6. y2: T2
7. x1 = y1
8. x2 = y2
9. < x1,x2 > = < y1,y2 >

False

By: ApFunToHypEquands `p' 2of(p) T2 9

Generated subgoal:

1 10. 2of( < x1,x2 > ) = 2of( < y1,y2 > )
False

About: