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

At: discrete union 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. x: T1+T2
6. y: T1+T2

Dec(x = y)
By:
UnfoldTopAb 0
THEN
Analyze 6
THEN
Analyze 5
Generated subgoals:

15. x2: T1
6. x1: T1
inl(x2) = inl(x1) T1+T2 inl(x2) = inl(x1) T1+T2
25. y: T2
6. x1: T1
inr(y) = inl(x1) T1+T2 inr(y) = inl(x1) T1+T2
35. x1: T1
6. y1: T2
inl(x1) = inr(y1) T1+T2 inl(x1) = inr(y1) T1+T2
45. y: T2
6. y1: T2
inr(y) = inr(y1) T1+T2 inr(y) = inr(y1) T1+T2

About:
decidableunioninlinruniverseequalorall

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