Nuprl - Pf discrete union 1 1 4

(27steps) 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. y: T2
6. y1: T2

inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2

By: With y (Analyze 4) THEN With y1 (Analyze -1) THEN Analyze -1

Generated subgoals:

1 4. y: T2
5. y1: T2
6. y = y1
inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2

2 4. y: T2
5. y1: T2
6. y = y1
inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2

About:

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

1	4. `y:` `T2` 5. `y1:` `T2` 6. `y = y1` `inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2`
2	4. `y:` `T2` 5. `y1:` `T2` 6. `y = y1` `inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2`