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

At: discrete union 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. x2: T1
6. x1: T1

inl(x2) = inl(x1) T1+T2 inl(x2) = inl(x1) T1+T2
By:
With x2 (Analyze 3)
THEN
With x1 (Analyze -1)
THEN
Analyze -1
Generated subgoals:

13. x,y:T2. Dec(x = y)
4. x2: T1
5. x1: T1
6. x2 = x1
inl(x2) = inl(x1) T1+T2 inl(x2) = inl(x1) T1+T2
23. x,y:T2. Dec(x = y)
4. x2: T1
5. x1: T1
6. x2 = x1
inl(x2) = inl(x1) T1+T2 inl(x2) = inl(x1) T1+T2

About:
decidableunioninluniverseequalorall

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