Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
. Discrete{T}
(
eq:{T
}.
u:T.
v:T List. v(
eq)(u::v))
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
. v(
eq)(u::v)
T:
. Discrete{T} 
(eq:{T
}. u:T. v:T List. v(
eq)(u::v))eq)(u::v)