Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T1:
.
T2:
{j}. Discrete{T1}
Discrete{T2}
Discrete{(T1
T2)}
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. Discrete{(T1
T2)}
T1:
. T2:{j}. Discrete{T1} 
Discrete{T2} Discrete{(T1 
T2)} T2)}