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

At: discrete union

T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1+T2)}
By: UnivCD
Generated subgoal:

11. T1: Type{i}
2. T2: Type{j}
3. Discrete{T1}
4. Discrete{T2}
Discrete{(T1+T2)}

About:
unionuniverseimpliesall

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