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