(20steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete product 1 1 1

1. T1: Type{i}
2. T2: Type{j}
3. x,y:T1. Dec(x = y)
4. x,y:T2. Dec(x = y)
5. x1: T1
6. x2: T2
7. y1: T1
8. y2: T2

< x1,x2 > = < y1,y2 > < x1,x2 > = < y1,y2 >

By:
Witness3 x1
THEN
With y1 (Analyze -1)
THEN
Analyze -1
THEN
Witness3 x2
THEN
With y2 (Analyze -1)
THEN
Analyze -1


Generated subgoals:

13. x1: T1
4. x2: T2
5. y1: T1
6. y2: T2
7. x1 = y1
8. x2 = y2
< x1,x2 > = < y1,y2 > < x1,x2 > = < y1,y2 >
23. x1: T1
4. x2: T2
5. y1: T1
6. y2: T2
7. x1 = y1
8. x2 = y2
< x1,x2 > = < y1,y2 > < x1,x2 > = < y1,y2 >
33. x1: T1
4. x2: T2
5. y1: T1
6. y2: T2
7. x1 = y1
8. x2 = y2
< x1,x2 > = < y1,y2 > < x1,x2 > = < y1,y2 >
43. x1: T1
4. x2: T2
5. y1: T1
6. y2: T2
7. x1 = y1
8. x2 = y2
< x1,x2 > = < y1,y2 > < x1,x2 > = < y1,y2 >

About:
pairproductdecidableuniverseequalorall

(20steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc