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