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) 
remove(eq;x;L) = M @ N)
Applied Tactic: D 0 THENA Auto THEN
D 0 THENA Auto THEN
DiscreteEq (-1) THEN
UnivCD THENA Auto
Generated subgoals:1. M,N:T List. L = M @ (x::N) remove(eq;x;L) = M @ N