Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. eq:{T=
}. u:T. L:T List. 
u(
eq) L 
(
v:T. M:T List. L = (v::M))
Applied Tactic: D 0 THENA Auto THEN
D 0 THENA Auto THEN
DiscreteEq (-1) THEN
UnivCD THENA Auto
Generated subgoals:1. v:T. M:T List. L = (v::M)