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

At: discrete union 1
1. T1: Type{i}
2. T2: Type{j}
3. Discrete{T1}
4. Discrete{T2}

Discrete{(T1+T2)}
By:
OnHyps [0;3;4] (i.UnfoldTopAb i)
THEN
UnivCD
Generated subgoal:

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

About:
decidableunionuniverseequal

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