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