Nuprl - Pf discrete product 1 1 1

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

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:

1 3. 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 >

2 3. 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 >

3 3. 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 >

4 3. 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:

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

1	3. `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 >`
2	3. `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 >`
3	3. `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 >`
4	3. `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 >`